--- a/NEWS Mon Aug 08 19:26:53 2011 -0700
+++ b/NEWS Tue Aug 09 07:44:17 2011 +0200
@@ -68,6 +68,8 @@
boolean algebras and complete linear orders. Lemmas Inf_less_iff,
less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
+Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary and Sup_binary have
+been discarded.
More consistent and less misunderstandable names:
INFI_def ~> INF_def
SUPR_def ~> SUP_def