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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
