diff -r 5fb07ec99828 -r cdf70f1fc9f9 NEWS
--- a/NEWS	Mon Sep 21 14:23:12 2009 +0200
+++ b/NEWS	Mon Sep 21 15:35:14 2009 +0200
@@ -102,7 +102,10 @@
     Complete_Lattice.UNION  (for SUPR)
   - object-logic definitions as far as appropriate
 
-  INCOMPATIBILITY.
+INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
+Un_subset_iff are explicitly deleted as default simp rules;  then
+also their lattice counterparts le_inf_iff and le_sup_iff have to be
+deleted to achieve the desired effect.
 
 * Power operations on relations and functions are now one dedicate
 constant "compow" with infix syntax "^^".  Power operations on