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

[Peter Lammich]

On Mi, 2012-10-17 at 11:09 +0200, Makarius wrote:
> *** ML ***
> 
> * Type Seq.results and related operations support embedded error
> messages within lazy enumerations, and thus allow to provide
> informative errors in the absence of any usable results.

Cool, no more writing of error messages to the trace buffer when
debugging tactics.


> Side remark:
> 
> Does anybody remember a use of the 'apply_end' command? Many years ago it 
> was introduced to help analyse the failure of 'qed', in symmetry to 
> 'apply' to break up 'proof' and 'by' steps.  That should now work without 
> it, just by letting 'qed' crash and looking at the error message.  Of 
> course, 'apply' has other uses and is not affected here.

I never knew it, but already got many questions from students whether
such a command exists, and I always denied it.


Peter