1.1 --- a/NEWS	Wed Jul 20 16:15:33 2011 +0200
     1.2 +++ b/NEWS	Wed Jul 20 22:14:39 2011 +0200
     1.3 @@ -63,15 +63,16 @@
     1.4  * Classes bot and top require underlying partial order rather than preorder:
     1.5  uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
     1.6  
     1.7 -* Class 'complete_lattice': generalized a couple of lemmas from sets;
     1.8 -generalized theorems INF_cong and SUP_cong.  More consistent and less
     1.9 -misunderstandable names:
    1.10 +* Class complete_lattice: generalized a couple of lemmas from sets;
    1.11 +generalized theorems INF_cong and SUP_cong.  New type classes for complete
    1.12 +boolean algebras and complete linear orderes.  Lemmas Inf_less_iff,
    1.13 +less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
    1.14 +More consistent and less misunderstandable names:
    1.15    INFI_def ~> INF_def
    1.16    SUPR_def ~> SUP_def
    1.17    le_SUPI ~> le_SUP_I
    1.18    le_SUPI2 ~> le_SUP_I2
    1.19    le_INFI ~> le_INF_I
    1.20 -  INF_subset ~> INF_superset_mono
    1.21    INFI_bool_eq ~> INF_bool_eq
    1.22    SUPR_bool_eq ~> SUP_bool_eq
    1.23    INFI_apply ~> INF_apply