# HG changeset patch
# User wenzelm
# Date 1316353195 -7200
# Node ID dfe923d5308dd02199343297ce34da6b98ee04d8
# Parent  7704b2fb02cc92e39e1127e59f3c19ef0d60b575
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);

diff -r 7704b2fb02cc -r dfe923d5308d NEWS
--- a/NEWS	Sun Sep 18 15:30:31 2011 +0200
+++ b/NEWS	Sun Sep 18 15:39:55 2011 +0200
@@ -113,6 +113,19 @@
 
 INCOMPATIBILITY.
 
+* Renamed theory Complete_Lattice to Complete_Lattices.
+INCOMPATIBILITY.
+
+* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,
+INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot,
+Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,
+Sup_insert are now declared as [simp].  INCOMPATIBILITY.
+
+* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,
+compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,
+sup_inf_absob, sup_left_idem are now declared as [simp].  Minor
+INCOMPATIBILITY.
+
 * Added syntactic classes "inf" and "sup" for the respective
 constants.  INCOMPATIBILITY: Changes in the argument order of the
 (mostly internal) locale predicates for some derived classes.
@@ -1651,26 +1664,12 @@
   INTER_fold_inter              ~> INFI_fold_inf
   UNION_fold_union              ~> SUPR_fold_sup
 
-* Theory "Complete_Lattice":
-
-  - renamed to "Complete_Lattices". minor INCOMPATIBILITY.
-
-  - lemmas top_def and bot_def have been replaced by the more convenient
-    lemmas Inf_empty and Sup_empty.  Dropped lemmas Inf_insert_simp and
-    Sup_insert_simp, which are subsumed by Inf_insert and Sup_insert.
-    Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ.
-    Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot
-    respectively.  INCOMPATIBILITY.
-
-  - lemmas Inf_eq_top_iff, INF_eq_top_iff, INF_image, Inf_insert, INF_top,
-    Inf_top_conv, INF_top_conv, SUP_bot, Sup_bot_conv, SUP_bot_conv,
-    Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, Sup_insert are now declared
-    as [simp]. minor INCOMPATIBILITY.
-
-* Theory "Lattice": lemmas compl_inf_bot, compl_le_comp_iff, compl_sup_top,
-inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, sup_inf_absob,
-sup_left_idem are now declared as [simp]. minor INCOMPATIBILITY.
-
+* Theory "Complete_Lattice": lemmas top_def and bot_def have been
+replaced by the more convenient lemmas Inf_empty and Sup_empty.
+Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
+by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
+former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
+subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
 
 * Reorganized theory Multiset: swapped notation of pointwise and
 multiset order: