[isabelle-dev] NEWS: more informative errors in lazy enumerations
andreas.lochbihler at kit.edu
Thu Oct 18 10:36:21 CEST 2012
> Side remark:
> 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. It usually saves me reprocessing the first 42 goals
when goal 43 needs another intro/simp/elim rule - and I can interactively
explore goal 43 immediately. Before I knew about apply_end, I used "case goal_43
thus ?case", but proof methods behave differently there, because the variables
are fixed in the context (e.g., tuples are not split automatically).
So I opt for keeping apply_end.
More information about the isabelle-dev