summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 64391 | 553d8c4d7ef4 |

parent 64390 | ad2c5f37f659 |

child 64439 | 2bafda87b524 |

child 64457 | f7aa4d0f7d02 |

--- a/NEWS Tue Oct 25 11:55:38 2016 +0200 +++ b/NEWS Tue Oct 25 12:14:17 2016 +0200 @@ -470,6 +470,34 @@ * Added class topological_monoid. +* The following theorems have been renamed: + + setsum_left_distrib ~> setsum_distrib_right + setsum_right_distrib ~> setsum_distrib_left + +INCOMPATIBILITY. + +* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. +INCOMPATIBILITY. + +* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional +comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` +A)". + +* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. + +* The type class ordered_comm_monoid_add is now called +ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add +is introduced as the combination of ordered_ab_semigroup_add + +comm_monoid_add. INCOMPATIBILITY. + +* Introduced the type classes canonically_ordered_comm_monoid_add and +dioid. + +* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When +instantiating linordered_semiring_strict and ordered_ab_group_add, an +explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might +be required. INCOMPATIBILITY. * Dropped various legacy fact bindings, whose replacements are often of a more general type also: @@ -646,16 +674,6 @@ * Session HOL-Probability: theory SPMF formalises discrete subprobability distributions. -* Session HOL-Number_Theory: algebraic foundation for primes: -Generalisation of predicate "prime" and introduction of predicates -"prime_elem", "irreducible", a "prime_factorization" function, and the -"factorial_ring" typeclass with instance proofs for nat, int, poly. Some -theorems now have different names, most notably "prime_def" is now -"prime_nat_iff". INCOMPATIBILITY. - -* Session Old_Number_Theory has been removed, after porting remaining -theories. - * Session HOL-Library: the names of multiset theorems have been normalised to distinguish which ordering the theorems are about @@ -685,35 +703,6 @@ Some functions have been renamed: ms_lesseq_impl -> subset_eq_mset_impl -* The following theorems have been renamed: - - setsum_left_distrib ~> setsum_distrib_right - setsum_right_distrib ~> setsum_distrib_left - -INCOMPATIBILITY. - -* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. -INCOMPATIBILITY. - -* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional -comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` -A)". - -* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. - -* The type class ordered_comm_monoid_add is now called -ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add -is introduced as the combination of ordered_ab_semigroup_add + -comm_monoid_add. INCOMPATIBILITY. - -* Introduced the type classes canonically_ordered_comm_monoid_add and -dioid. - -* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When -instantiating linordered_semiring_strict and ordered_ab_group_add, an -explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might -be required. INCOMPATIBILITY. - * HOL-Library: multisets are now ordered with the multiset ordering #\<subseteq># ~> \<le> #\<subset># ~> < @@ -886,7 +875,7 @@ empty_inter [simp] ~> [] INCOMPATIBILITY. -* Session HOL-Library, theory Multiset: The order of the variables in +* Session HOL-Library, theory Multiset: the order of the variables in the second cases of multiset_induct, multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A). INCOMPATIBILITY. @@ -933,6 +922,16 @@ Added theory of longest common prefixes. +* Session HOL-Number_Theory: algebraic foundation for primes: +Generalisation of predicate "prime" and introduction of predicates +"prime_elem", "irreducible", a "prime_factorization" function, and the +"factorial_ring" typeclass with instance proofs for nat, int, poly. Some +theorems now have different names, most notably "prime_def" is now +"prime_nat_iff". INCOMPATIBILITY. + +* Session Old_Number_Theory has been removed, after porting remaining +theories. + *** ML ***