1.1 --- a/NEWS	Thu Sep 15 10:57:40 2011 +0200
     1.2 +++ b/NEWS	Thu Sep 15 17:06:00 2011 +0200
     1.3 @@ -1650,12 +1650,26 @@
     1.4    INTER_fold_inter              ~> INFI_fold_inf
     1.5    UNION_fold_union              ~> SUPR_fold_sup
     1.6  
     1.7 -* Theory "Complete_Lattice": lemmas top_def and bot_def have been
     1.8 -replaced by the more convenient lemmas Inf_empty and Sup_empty.
     1.9 -Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
    1.10 -by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
    1.11 -former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
    1.12 -subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
    1.13 +* Theory "Complete_Lattice":
    1.14 +
    1.15 +  - renamed to "Complete_Lattices". minor INCOMPATIBILITY.
    1.16 +
    1.17 +  - lemmas top_def and bot_def have been replaced by the more convenient
    1.18 +    lemmas Inf_empty and Sup_empty.  Dropped lemmas Inf_insert_simp and
    1.19 +    Sup_insert_simp, which are subsumed by Inf_insert and Sup_insert.
    1.20 +    Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ and Sup_Univ.
    1.21 +    Lemmas inf_top_right and sup_bot_right subsume inf_top and sup_bot
    1.22 +    respectively.  INCOMPATIBILITY.
    1.23 +
    1.24 +  - lemmas Inf_eq_top_iff, INF_eq_top_iff, INF_image, Inf_insert, INF_top,
    1.25 +    Inf_top_conv, INF_top_conv, SUP_bot, Sup_bot_conv, SUP_bot_conv,
    1.26 +    Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, Sup_insert are now declared
    1.27 +    as [simp]. minor INCOMPATIBILITY.
    1.28 +
    1.29 +* Theory "Lattice": lemmas compl_inf_bot, compl_le_comp_iff, compl_sup_top,
    1.30 +inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, sup_inf_absob,
    1.31 +sup_left_idem are now declared as [simp]. minor INCOMPATIBILITY.
    1.32 +
    1.33  
    1.34  * Reorganized theory Multiset: swapped notation of pointwise and
    1.35  multiset order: