summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 18 Sep 2011 15:39:55 +0200 | |

changeset 44973 | dfe923d5308d |

parent 44972 | 7704b2fb02cc |

child 44974 | 7762718f5e89 |

separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);

--- 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: