--- 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