[isabelle-dev] NEWS: more informative errors in lazy enumerations

[Andreas Lochbihler]

Hi Makarius,

 > 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.

Andreas