# [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.*