1.1 --- a/NEWS	Fri Mar 06 14:51:18 2009 +0100
     1.2 +++ b/NEWS	Fri Mar 06 15:51:18 2009 +0100
     1.3 @@ -224,6 +224,21 @@
     1.4  With strict functions on linear orders, reasoning about (in)equalities is
     1.5  facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less".
     1.6  
     1.7 +* Some set operations are now proper qualified constants with authentic syntax.
     1.8 +INCOMPATIBILITY:
     1.9 +
    1.10 +    op Int ~>   Set.Int
    1.11 +    op Un ~>    Set.Un
    1.12 +    INTER ~>    Set.INTER
    1.13 +    UNION ~>    Set.UNION
    1.14 +    Inter ~>    Set.Inter
    1.15 +    Union ~>    Set.Union
    1.16 +    {} ~>       Set.empty
    1.17 +    UNIV ~>     Set.UNIV
    1.18 +
    1.19 +* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in theory
    1.20 +Set.
    1.21 +
    1.22  * Auxiliary class "itself" has disappeared -- classes without any parameter
    1.23  are treated as expected by the 'class' command.
    1.24  
    1.25 @@ -301,7 +316,7 @@
    1.26  avoiding strange error messages.
    1.27  
    1.28  * Simplifier: simproc for let expressions now unfolds if bound variable
    1.29 -occurs at most one time in let expression body.  INCOMPATIBILITY.
    1.30 +occurs at most once in let expression body.  INCOMPATIBILITY.
    1.31  
    1.32  * New classes "top" and "bot" with corresponding operations "top" and "bot"
    1.33  in theory Orderings;  instantiation of class "complete_lattice" requires