[isabelle] Fwd: Fw: How to apply a theorem?




-------- Пересылаемое сообщение --------
14.03.09, 22:18, "Victor Porton" <porton at narod.ru>:

14.03.09, 21:01, "Slawomir Kolodynski" <skokodyn at yahoo.com>:

> > Slawomir, your solution may fail if small and big aren't
> > disjoint.
> True. A better definition would be
> definition
> "Emedding(embed, small, big) \<equiv> 
> (small - big) \<union> (big - embed``(small - big))"

What is "``"? I'm a novice with Isabelle and don't understand two backquotes.

> > definition "ret == converse(move)"
> I don't understand this definition. The right hand side depends on a variable "move" and the left hand does not. Is "move" a constant? How it is defined?

"move" should be a constant. It will be defined in a somehow tricky way. For now we can use the stub definition:

definition "move == 0" (*to be replaced with the real definition*)
-------- Завершение пересылаемого сообщения --------





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.