--- 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.