1.1 --- a/NEWS	Wed Nov 24 10:39:58 2010 +0100
     1.2 +++ b/NEWS	Wed Nov 24 10:42:28 2010 +0100
     1.3 @@ -89,6 +89,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Enum (for explicit enumerations of finite types) is now part of
     1.8 +the HOL-Main image. INCOMPATIBILITY: All constants of the Enum theory now 
     1.9 +have to be referred to by its qualified name.
    1.10 +  constants
    1.11 +    enum -> Enum.enum
    1.12 +    nlists -> Enum.nlists
    1.13 +    product -> Enum.product
    1.14 +
    1.15  * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
    1.16  avoid confusion with finite sets.  INCOMPATIBILITY.
    1.17