[isabelle-dev] on the fly theorems for Isar

[Mamoun FILALI-AMINE]

   Is it possible to have an "on the fly" facility for Isar:
   currently we have to remember theorem names in order to reuse them
   the onthefly would prove again the given theorem on the fly
   example:
   instead of
       unfolding imp_disjL
   one would write
      unfolding (onthefly "(a \/ b --> c) = ((a --> c) /\ (b --> c))")

Mamoun


-------------- next part --------------
A non-text attachment was scrubbed...
Name: filali.vcf
Type: text/x-vcard
Size: 277 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100417/475c865f/attachment-0002.vcf>