1.1 --- a/NEWS	Mon Sep 12 09:45:53 2011 +0200
     1.2 +++ b/NEWS	Mon Sep 12 10:27:36 2011 +0200
     1.3 @@ -230,6 +230,18 @@
     1.4  * Well-founded recursion combinator "wfrec" has been moved to theory
     1.5  Library/Wfrec. INCOMPATIBILITY.
     1.6  
     1.7 +* Theory HOL/Library/Cset_Monad allows do notation for computable
     1.8 +  sets (cset) via the generic monad ad-hoc overloading facility.
     1.9 +
    1.10 +* Theories of common data structures are split into theories for
    1.11 +  implementation, an invariant-ensuring type, and connection to
    1.12 +  an abstract type. INCOMPATIBILITY.
    1.13 +
    1.14 +  - RBT is split into RBT and RBT_Mapping.
    1.15 +  - AssocList is split and renamed into AList_Impl and AList_Mapping.
    1.16 +  - DList is split into DList_Impl, DList, and DList_Cset.
    1.17 +  - Cset is split into Cset and List_Cset.
    1.18 +  
    1.19  * Theory Library/Nat_Infinity has been renamed to
    1.20  Library/Extended_Nat, with name changes of the following types and
    1.21  constants: