[isabelle-dev] NEWS: more informative errors in lazy enumerations
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
> 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