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
<<attachment: filali.vcf>>
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
