NEWS
changeset 32217 420108dd7dfe
parent 32216 2f3d65d15149
child 32235 8f9b8d14fc9f
     1.1 --- a/NEWS	Sun Jul 26 22:33:32 2009 +0200
     1.2 +++ b/NEWS	Mon Jul 27 09:01:13 2009 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  * New quickcheck implementation using new code generator.
     1.6  
     1.7 -* New type class boolean_algebra.
     1.8 +* New class "boolean_algebra".
     1.9  
    1.10  * Refinements to lattices classes:
    1.11    - added boolean_algebra type class
    1.12 @@ -40,6 +40,19 @@
    1.13    - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
    1.14    - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
    1.15    - renamed ACI to inf_sup_aci
    1.16 +  - class "complete_lattice" moved to separate theory "complete_lattice";
    1.17 +    corresponding constants renamed:
    1.18 +    
    1.19 +    Set.Inf ~>      Complete_Lattice.Inf
    1.20 +    Set.Sup ~>      Complete_Lattice.Sup
    1.21 +    Set.INFI ~>     Complete_Lattice.INFI
    1.22 +    Set.SUPR ~>     Complete_Lattice.SUPR
    1.23 +    Set.Inter ~>    Complete_Lattice.Inter
    1.24 +    Set.Union ~>    Complete_Lattice.Union
    1.25 +    Set.INTER ~>    Complete_Lattice.INTER
    1.26 +    Set.UNION ~>    Complete_Lattice.UNION
    1.27 +
    1.28 +  INCOMPATIBILITY.
    1.29  
    1.30  * Class semiring_div requires superclass no_zero_divisors and proof of
    1.31  div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,