# HG changeset patch # User noschinl # Date 1316099160 -7200 # Node ID e1139e612b5551c39b3d957d58352d8fff4fe1ec # Parent 2e812384afa83e645d143394b810dfe0dc530eeb NEWS on Complete_Lattices, Lattices diff -r 2e812384afa8 -r e1139e612b55 NEWS --- a/NEWS Thu Sep 15 10:57:40 2011 +0200 +++ b/NEWS Thu Sep 15 17:06:00 2011 +0200 @@ -1650,12 +1650,26 @@ INTER_fold_inter ~> INFI_fold_inf UNION_fold_union ~> SUPR_fold_sup -* 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. +* 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. + * Reorganized theory Multiset: swapped notation of pointwise and multiset order: