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