diff -r c553044e8a3e -r 8b55b9c986a4 NEWS
--- a/NEWS	Mon Sep 12 09:45:53 2011 +0200
+++ b/NEWS	Mon Sep 12 10:27:36 2011 +0200
@@ -230,6 +230,18 @@
 * Well-founded recursion combinator "wfrec" has been moved to theory
 Library/Wfrec. INCOMPATIBILITY.
 
+* Theory HOL/Library/Cset_Monad allows do notation for computable
+  sets (cset) via the generic monad ad-hoc overloading facility.
+
+* Theories of common data structures are split into theories for
+  implementation, an invariant-ensuring type, and connection to
+  an abstract type. INCOMPATIBILITY.
+
+  - RBT is split into RBT and RBT_Mapping.
+  - AssocList is split and renamed into AList_Impl and AList_Mapping.
+  - DList is split into DList_Impl, DList, and DList_Cset.
+  - Cset is split into Cset and List_Cset.
+  
 * Theory Library/Nat_Infinity has been renamed to
 Library/Extended_Nat, with name changes of the following types and
 constants: