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

author | wenzelm |

Mon, 07 Jun 2021 14:40:22 +0200 | |

changeset 73829 | aefa7d210725 |

parent 73828 | 201200b549fc |

child 73830 | 2a431e8bb9b4 |

more formal theory and session names;
tuned whitespace;

--- a/NEWS Mon Jun 07 14:34:55 2021 +0200 +++ b/NEWS Mon Jun 07 14:40:22 2021 +0200 @@ -105,14 +105,14 @@ *** HOL *** -* Theory Multiset: dedicated predicate "multiset" is gone, use -explict expression instead. Minor INCOMPATIBILITY. - -* Theory Multiset: consolidated abbreviations Mempty, Melem, not_Melem -to empty_mset, member_mset, not_member_mset respectively. Minor -INCOMPATIBILITY. - -* Theory Multiset: consolidated operation and fact names: +* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone, +use explict expression instead. Minor INCOMPATIBILITY. + +* Theory "HOL-Library.Multiset": consolidated abbreviations Mempty, +Melem, not_Melem to empty_mset, member_mset, not_member_mset +respectively. Minor INCOMPATIBILITY. + +* Theory "HOL-Library.Multiset": consolidated operation and fact names: inf_subset_mset ~> inter_mset sup_subset_mset ~> union_mset multiset_inter_def ~> inter_mset_def @@ -120,52 +120,52 @@ multiset_inter_count ~> count_inter_mset sup_subset_mset_count ~> count_union_mset -* Theory Multiset: syntax precendence for membership operations has been -adjusted to match the corresponding precendences on sets. Rare -INCOMPATIBILITY. - -* HOL-Analysis/HOL-Probability: indexed products of discrete -distributions, negative binomial distribution, Hoeffding's inequality, -Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some -more small lemmas. Some theorems that were stated awkwardly before were -corrected. Minor INCOMPATIBILITY. +* Theory "HOL-Library.Multiset": syntax precendence for membership +operations has been adjusted to match the corresponding precendences on +sets. Rare INCOMPATIBILITY. + +* Session "HOL-Analysis" and "HOL-Probability": indexed products of +discrete distributions, negative binomial distribution, Hoeffding's +inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, +and some more small lemmas. Some theorems that were stated awkwardly +before were corrected. Minor INCOMPATIBILITY. * Theorems "antisym" and "eq_iff" in class "order" have been renamed to "order.antisym" and "order.eq_iff", to coexist locally with "antisym" -and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant +and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant potential for change can be avoided if interpretations of type class "order" are replaced or augmented by interpretations of locale "ordering". -* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor +* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor INCOMPATIBILITY; note that for most applications less elementary lemmas exists. -* Dedicated session HOL-Combinatorics. INCOMPATIBILITY: theories +* Theory "HOL-Library.Permutation" has been renamed to the more specific +"HOL-Library.List_Permutation". Note that most notions from that theory +are already present in theory "HOL-Combinatorics.Permutations". +INCOMPATIBILITY. + +* Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling", "Multiset_Permutations", "Perm" have been moved there from session HOL-Library. -* Theory "Permutation" in HOL-Library has been renamed to the more -specific "List_Permutation". Note that most notions from that -theory are already present in theory "Permutations". INCOMPATIBILITY. - -* Lemma "permutes_induct" has been given stronger -hypotheses and named premises. INCOMPATIBILITY. - -* Theory "Transposition" in HOL-Combinatorics provides elementary -swap operation "transpose". - -* Combinator "Fun.swap" resolved into a mere input abbreviation -in separate theory "Transposition" in HOL-Combinatorics. -INCOMPATIBILITY. +* Theory "HOL-Combinatorics.Transposition" provides elementary swap +operation "transpose". + +* Lemma "permutes_induct" has been given stronger hypotheses and named +premises. INCOMPATIBILITY. + +* Combinator "Fun.swap" resolved into a mere input abbreviation in +separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY. * Bit operations set_bit, unset_bit and flip_bit are now class -operations. INCOMPATIBILITY. +operations. INCOMPATIBILITY. * Abbreviation "max_word" has been moved to session Word_Lib in the AFP, as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", -"setBit", "clearBit". See there further the changelog in theory Guide. +"setBit", "clearBit". See there further the changelog in theory Guide. INCOMPATIBILITY.