1.1 --- a/NEWS	Tue Oct 16 21:26:36 2012 +0200
     1.2 +++ b/NEWS	Tue Oct 16 21:30:52 2012 +0200
     1.3 @@ -41,6 +41,9 @@
     1.4  specifications: nesting of "context fixes ... context assumes ..."
     1.5  and "class ... context ...".
     1.6  
     1.7 +* More informative error messages for Isar proof commands involving
     1.8 +lazy enumerations (method applications etc.).
     1.9 +
    1.10  
    1.11  *** Pure ***
    1.12  
    1.13 @@ -201,6 +204,10 @@
    1.14  
    1.15  *** ML ***
    1.16  
    1.17 +* Type Seq.results and related operations support embedded error
    1.18 +messages within lazy enumerations, and thus allow to provide
    1.19 +informative errors in the absence of any usable results.
    1.20 +
    1.21  * Renamed Position.str_of to Position.here to emphasize that this is a
    1.22  formal device to inline positions into message text, but not
    1.23  necessarily printing visible text.