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