# HG changeset patch
# User haftmann
# Date 1264163920 -3600
# Node ID aa5d27f1d9b914423768a123850c4b0db689a293
# Parent  478f31081a785ee7b98965757bf8b10a6eb20a93
NEWS

diff -r 478f31081a78 -r aa5d27f1d9b9 NEWS
--- 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.