diff -r aa04d1e1e2cc -r 26ca0bad226a NEWS
--- 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