1.1 --- a/NEWS	Wed Nov 19 18:15:31 2008 +0100
     1.2 +++ b/NEWS	Thu Nov 20 00:03:47 2008 +0100
     1.3 @@ -47,6 +47,11 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Slightly more coherent Pure syntax, with updated documentation in
     1.8 +isar-ref manual.  Removed locales meta_term_syntax and
     1.9 +meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
    1.10 +INCOMPATIBILITY in rare situations.
    1.11 +
    1.12  * Goal-directed proof now enforces strict proof irrelevance wrt. sort
    1.13  hypotheses.  Sorts required in the course of reasoning need to be
    1.14  covered by the constraints in the initial statement, completed by the