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




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

Hi Slawomir,

theorem ret_th: shows "converse(move): bij(newbig, big)"
using move_th bij_converse_bij by simp;

does work, but

theorem ret_th: shows "ret: bij(newbig, big)"
using move_th bij_converse_bij by simp;

does not work.

How to make the last case to work?

14.03.09, 22:24, "Slawomir Kolodynski" <skokodyn at yahoo.com>:

> Victor,
> > theory does not work
> That is surprising. I have run it through Isabelle and it verifies fine on my machine. I am using the official release of Isabelle 2008. I attach the full theory just to make sure there is no copy-paste mistake.
> Slawek
>       
-------- Завершение пересылаемого сообщения --------





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