>> Does anybody remember a use of the 'apply_end' command? > Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although > they could be fused into the qed. However, I regularly use apply_end > when I develop the method call for qed to finish off all the remaining > cases after having dealt with the interesting ones.
I sometimes use a similar pattern, although in my situations a rewrite
from apply … proof … to proof … qed … is no problem. So, I personally
do not care about, but I acknowledge Andreas' use case.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
