NEWS
changeset 73829 aefa7d210725
parent 73828 201200b549fc
child 73830 2a431e8bb9b4
equal deleted inserted replaced
73828:201200b549fc 73829:aefa7d210725
   103 no longer required.
   103 no longer required.
   104 
   104 
   105 
   105 
   106 *** HOL ***
   106 *** HOL ***
   107 
   107 
   108 * Theory Multiset: dedicated predicate "multiset" is gone, use
   108 * Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
   109 explict expression instead.  Minor INCOMPATIBILITY.
   109 use explict expression instead. Minor INCOMPATIBILITY.
   110 
   110 
   111 * Theory Multiset: consolidated abbreviations Mempty, Melem, not_Melem
   111 * Theory "HOL-Library.Multiset": consolidated abbreviations Mempty,
   112 to empty_mset, member_mset, not_member_mset respectively.  Minor
   112 Melem, not_Melem to empty_mset, member_mset, not_member_mset
   113 INCOMPATIBILITY.
   113 respectively. Minor INCOMPATIBILITY.
   114 
   114 
   115 * Theory Multiset: consolidated operation and fact names:
   115 * Theory "HOL-Library.Multiset": consolidated operation and fact names:
   116     inf_subset_mset ~> inter_mset
   116     inf_subset_mset ~> inter_mset
   117     sup_subset_mset ~> union_mset
   117     sup_subset_mset ~> union_mset
   118     multiset_inter_def ~> inter_mset_def
   118     multiset_inter_def ~> inter_mset_def
   119     sup_subset_mset_def ~> union_mset_def
   119     sup_subset_mset_def ~> union_mset_def
   120     multiset_inter_count ~> count_inter_mset
   120     multiset_inter_count ~> count_inter_mset
   121     sup_subset_mset_count ~> count_union_mset
   121     sup_subset_mset_count ~> count_union_mset
   122 
   122 
   123 * Theory Multiset: syntax precendence for membership operations has been
   123 * Theory "HOL-Library.Multiset": syntax precendence for membership
   124 adjusted to match the corresponding precendences on sets.  Rare
   124 operations has been adjusted to match the corresponding precendences on
   125 INCOMPATIBILITY.
   125 sets. Rare INCOMPATIBILITY.
   126 
   126 
   127 * HOL-Analysis/HOL-Probability: indexed products of discrete
   127 * Session "HOL-Analysis" and "HOL-Probability": indexed products of
   128 distributions, negative binomial distribution, Hoeffding's inequality,
   128 discrete distributions, negative binomial distribution, Hoeffding's
   129 Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some
   129 inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
   130 more small lemmas. Some theorems that were stated awkwardly before were
   130 and some more small lemmas. Some theorems that were stated awkwardly
   131 corrected. Minor INCOMPATIBILITY.
   131 before were corrected. Minor INCOMPATIBILITY.
   132 
   132 
   133 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to
   133 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to
   134 "order.antisym" and "order.eq_iff", to coexist locally with "antisym"
   134 "order.antisym" and "order.eq_iff", to coexist locally with "antisym"
   135 and "eq_iff" from locale "ordering".  INCOMPATIBILITY: significant
   135 and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
   136 potential for change can be avoided if interpretations of type class
   136 potential for change can be avoided if interpretations of type class
   137 "order" are replaced or augmented by interpretations of locale
   137 "order" are replaced or augmented by interpretations of locale
   138 "ordering".
   138 "ordering".
   139 
   139 
   140 * Theorem "swap_def" now is always qualified as "Fun.swap_def".  Minor
   140 * Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
   141 INCOMPATIBILITY; note that for most applications less elementary lemmas
   141 INCOMPATIBILITY; note that for most applications less elementary lemmas
   142 exists.
   142 exists.
   143 
   143 
   144 * Dedicated session HOL-Combinatorics.  INCOMPATIBILITY: theories
   144 * Theory "HOL-Library.Permutation" has been renamed to the more specific
       
   145 "HOL-Library.List_Permutation". Note that most notions from that theory
       
   146 are already present in theory "HOL-Combinatorics.Permutations".
       
   147 INCOMPATIBILITY.
       
   148 
       
   149 * Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories
   145 "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
   150 "Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
   146 "Multiset_Permutations", "Perm" have been moved there from session
   151 "Multiset_Permutations", "Perm" have been moved there from session
   147 HOL-Library.
   152 HOL-Library.
   148 
   153 
   149 * Theory "Permutation" in HOL-Library has been renamed to the more
   154 * Theory "HOL-Combinatorics.Transposition" provides elementary swap
   150 specific "List_Permutation".  Note that most notions from that
   155 operation "transpose".
   151 theory are already present in theory "Permutations".  INCOMPATIBILITY.
   156 
   152 
   157 * Lemma "permutes_induct" has been given stronger hypotheses and named
   153 * Lemma "permutes_induct" has been given stronger
   158 premises. INCOMPATIBILITY.
   154 hypotheses and named premises.  INCOMPATIBILITY.
   159 
   155 
   160 * Combinator "Fun.swap" resolved into a mere input abbreviation in
   156 * Theory "Transposition" in HOL-Combinatorics provides elementary
   161 separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
   157 swap operation "transpose".
       
   158 
       
   159 * Combinator "Fun.swap" resolved into a mere input abbreviation
       
   160 in separate theory "Transposition" in HOL-Combinatorics.
       
   161 INCOMPATIBILITY.
       
   162 
   162 
   163 * Bit operations set_bit, unset_bit and flip_bit are now class
   163 * Bit operations set_bit, unset_bit and flip_bit are now class
   164 operations.  INCOMPATIBILITY.
   164 operations. INCOMPATIBILITY.
   165 
   165 
   166 * Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
   166 * Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
   167 as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
   167 as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
   168 "setBit", "clearBit".  See there further the changelog in theory Guide.
   168 "setBit", "clearBit". See there further the changelog in theory Guide.
   169 INCOMPATIBILITY.
   169 INCOMPATIBILITY.
   170 
   170 
   171 
   171 
   172 *** ML ***
   172 *** ML ***
   173 
   173