diff -r 4588597ba37e -r 81e55342cb86 NEWS
--- a/NEWS	Mon Aug 08 08:55:49 2011 -0700
+++ b/NEWS	Mon Aug 08 19:21:11 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