1.1 --- a/NEWS Sun Sep 18 15:30:31 2011 +0200
1.2 +++ b/NEWS Sun Sep 18 15:39:55 2011 +0200
1.3 @@ -113,6 +113,19 @@
1.4
1.5 INCOMPATIBILITY.
1.6
1.7 +* Renamed theory Complete_Lattice to Complete_Lattices.
1.8 +INCOMPATIBILITY.
1.9 +
1.10 +* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,
1.11 +INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot,
1.12 +Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,
1.13 +Sup_insert are now declared as [simp]. INCOMPATIBILITY.
1.14 +
1.15 +* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,
1.16 +compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,
1.17 +sup_inf_absob, sup_left_idem are now declared as [simp]. Minor
1.18 +INCOMPATIBILITY.
1.19 +
1.20 * Added syntactic classes "inf" and "sup" for the respective
1.21 constants. INCOMPATIBILITY: Changes in the argument order of the
1.22 (mostly internal) locale predicates for some derived classes.
1.23 @@ -1651,26 +1664,12 @@
1.24 INTER_fold_inter ~> INFI_fold_inf
1.25 UNION_fold_union ~> SUPR_fold_sup
1.26
1.27 -* Theory "Complete_Lattice":
1.28 -
1.29 - - renamed to "Complete_Lattices". minor INCOMPATIBILITY.
1.30 -
1.31 - - lemmas top_def and bot_def have been replaced by the more convenient
1.32 - lemmas Inf_empty and Sup_empty. Dropped lemmas Inf_insert_simp and
1.33 - Sup_insert_simp, which are subsumed by Inf_insert and Sup_insert.
1.34 - Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ.
1.35 - Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot
1.36 - respectively. INCOMPATIBILITY.
1.37 -
1.38 - - lemmas Inf_eq_top_iff, INF_eq_top_iff, INF_image, Inf_insert, INF_top,
1.39 - Inf_top_conv, INF_top_conv, SUP_bot, Sup_bot_conv, SUP_bot_conv,
1.40 - Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, Sup_insert are now declared
1.41 - as [simp]. minor INCOMPATIBILITY.
1.42 -
1.43 -* Theory "Lattice": lemmas compl_inf_bot, compl_le_comp_iff, compl_sup_top,
1.44 -inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, sup_inf_absob,
1.45 -sup_left_idem are now declared as [simp]. minor INCOMPATIBILITY.
1.46 -
1.47 +* Theory "Complete_Lattice": lemmas top_def and bot_def have been
1.48 +replaced by the more convenient lemmas Inf_empty and Sup_empty.
1.49 +Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
1.50 +by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace
1.51 +former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right
1.52 +subsume inf_top and sup_bot respectively. INCOMPATIBILITY.
1.53
1.54 * Reorganized theory Multiset: swapped notation of pointwise and
1.55 multiset order: