NEWS
changeset 49869 bd370af308f0
parent 49841 18cb42182d3e
child 49918 cf441f4a358b
--- 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.