separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
authorwenzelm
Sun Sep 18 15:39:55 2011 +0200 (2011-09-18)
changeset 44973dfe923d5308d
parent 44972 7704b2fb02cc
child 44974 7762718f5e89
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
NEWS
     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: