1.1 --- a/NEWS	Tue Aug 17 14:19:12 2010 +0200
     1.2 +++ b/NEWS	Tue Aug 17 14:33:39 2010 +0200
     1.3 @@ -35,11 +35,17 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10 +* Quickcheck in locales considers interpretations of that locale for
    1.11 +counter example search.
    1.12 +
    1.13  * Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
    1.14  in Library/State_Monad has been changed to avoid ambiguities.
    1.15  INCOMPATIBILITY.
    1.16  
    1.17 -* code generator: export_code without explicit file declaration prints
    1.18 +* Code generator: export_code without explicit file declaration prints
    1.19  to standard output.  INCOMPATIBILITY.
    1.20  
    1.21  * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
    1.22 @@ -121,8 +127,8 @@
    1.23  INCOMPATIBILITY.
    1.24  
    1.25  * Inductive package: offers new command "inductive_simps" to automatically
    1.26 -  derive instantiated and simplified equations for inductive predicates,
    1.27 -  similar to inductive_cases.
    1.28 +derive instantiated and simplified equations for inductive predicates,
    1.29 +similar to inductive_cases.
    1.30  
    1.31  
    1.32  *** ML ***