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

Peter Lammich lammich at in.tum.de
Wed Oct 17 11:45:40 CEST 2012

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.


More information about the isabelle-dev mailing list