1.1 --- a/NEWS	Fri Jan 22 13:38:29 2010 +0100
     1.2 +++ b/NEWS	Fri Jan 22 13:38:40 2010 +0100
     1.3 @@ -12,6 +12,15 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Various old-style primrec specifications in the HOL theories have been
     1.8 +replaced by new-style primrec, especially in theory List.  The corresponding
     1.9 +constants now have authentic syntax.  INCOMPATIBILITY.
    1.10 +
    1.11 +* Reorganized theory Multiset.thy: less duplication, less historical
    1.12 +organization of sections, conversion from associations lists to
    1.13 +multisets, rudimentary code generation.  Use insert_DiffM2 [symmetric]
    1.14 +instead of elem_imp_eq_diff_union, if needed.  INCOMPATIBILITY.
    1.15 +
    1.16  * Reorganized theory Sum_Type.thy; Inl and Inr now have
    1.17  authentic syntax.  INCOMPATIBILITY.
    1.18