NEWS

 in old "ref" manual.
 
 * Improved support for auxiliary contexts indicate block structure for
 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 ***
 
 * Code generation for Haskell: restrict unqualified imports from

 * Simplified custom document/build script, instead of old-style
 document/IsaMakefile.  Minor INCOMPATIBILITY.
 
 
 *** 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.