NEWS
changeset 32066 091f1e304120
parent 31997 de0d280c31a7
parent 32064 53ca12ff305d
child 32079 5dc52b199815
     1.1 --- a/NEWS	Tue Jul 14 12:18:52 2009 +0200
     1.2 +++ b/NEWS	Tue Jul 14 15:55:27 2009 +0200
     1.3 @@ -28,6 +28,14 @@
     1.4  
     1.5  * New type class boolean_algebra.
     1.6  
     1.7 +* Refinements to lattices classes:
     1.8 +  - added boolean_algebra type class
     1.9 +  - less default intro/elim rules in locale variant, more default
    1.10 +    intro/elim rules in class variant: more uniformity
    1.11 +  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
    1.12 +  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
    1.13 +  - renamed ACI to inf_sup_aci
    1.14 +
    1.15  * Class semiring_div requires superclass no_zero_divisors and proof of
    1.16  div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
    1.17  div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been