# HG changeset patch
# User wenzelm
# Date 1350415852 -7200
# Node ID bd370af308f00071c8c610e1304d3e90f90bd3df
# Parent  3039922ffd8def7f985b2625dc78c4d43475bd25
support for more informative errors in lazy enumerations;

diff -r 3039922ffd8d -r bd370af308f0 NEWS
--- a/NEWS	Tue Oct 16 21:26:36 2012 +0200
+++ b/NEWS	Tue Oct 16 21:30:52 2012 +0200
@@ -41,6 +41,9 @@
 specifications: nesting of "context fixes ... context assumes ..."
 and "class ... context ...".
 
+* More informative error messages for Isar proof commands involving
+lazy enumerations (method applications etc.).
+
 
 *** Pure ***
 
@@ -201,6 +204,10 @@
 
 *** 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.
+
 * Renamed Position.str_of to Position.here to emphasize that this is a
 formal device to inline positions into message text, but not
 necessarily printing visible text.