author | wenzelm |

Tue Oct 25 12:14:17 2016 +0200 (2016-10-25) | |

changeset 64391 | 553d8c4d7ef4 |

parent 64390 | ad2c5f37f659 |

child 64392 | 9456313b57ed |

tuned;

1.1 --- a/NEWS Tue Oct 25 11:55:38 2016 +0200 1.2 +++ b/NEWS Tue Oct 25 12:14:17 2016 +0200 1.3 @@ -470,6 +470,34 @@ 1.4 1.5 * Added class topological_monoid. 1.6 1.7 +* The following theorems have been renamed: 1.8 + 1.9 + setsum_left_distrib ~> setsum_distrib_right 1.10 + setsum_right_distrib ~> setsum_distrib_left 1.11 + 1.12 +INCOMPATIBILITY. 1.13 + 1.14 +* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. 1.15 +INCOMPATIBILITY. 1.16 + 1.17 +* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional 1.18 +comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` 1.19 +A)". 1.20 + 1.21 +* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 1.22 + 1.23 +* The type class ordered_comm_monoid_add is now called 1.24 +ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 1.25 +is introduced as the combination of ordered_ab_semigroup_add + 1.26 +comm_monoid_add. INCOMPATIBILITY. 1.27 + 1.28 +* Introduced the type classes canonically_ordered_comm_monoid_add and 1.29 +dioid. 1.30 + 1.31 +* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 1.32 +instantiating linordered_semiring_strict and ordered_ab_group_add, an 1.33 +explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 1.34 +be required. INCOMPATIBILITY. 1.35 1.36 * Dropped various legacy fact bindings, whose replacements are often 1.37 of a more general type also: 1.38 @@ -646,16 +674,6 @@ 1.39 * Session HOL-Probability: theory SPMF formalises discrete 1.40 subprobability distributions. 1.41 1.42 -* Session HOL-Number_Theory: algebraic foundation for primes: 1.43 -Generalisation of predicate "prime" and introduction of predicates 1.44 -"prime_elem", "irreducible", a "prime_factorization" function, and the 1.45 -"factorial_ring" typeclass with instance proofs for nat, int, poly. Some 1.46 -theorems now have different names, most notably "prime_def" is now 1.47 -"prime_nat_iff". INCOMPATIBILITY. 1.48 - 1.49 -* Session Old_Number_Theory has been removed, after porting remaining 1.50 -theories. 1.51 - 1.52 * Session HOL-Library: the names of multiset theorems have been 1.53 normalised to distinguish which ordering the theorems are about 1.54 1.55 @@ -685,35 +703,6 @@ 1.56 Some functions have been renamed: 1.57 ms_lesseq_impl -> subset_eq_mset_impl 1.58 1.59 -* The following theorems have been renamed: 1.60 - 1.61 - setsum_left_distrib ~> setsum_distrib_right 1.62 - setsum_right_distrib ~> setsum_distrib_left 1.63 - 1.64 -INCOMPATIBILITY. 1.65 - 1.66 -* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. 1.67 -INCOMPATIBILITY. 1.68 - 1.69 -* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional 1.70 -comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` 1.71 -A)". 1.72 - 1.73 -* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 1.74 - 1.75 -* The type class ordered_comm_monoid_add is now called 1.76 -ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 1.77 -is introduced as the combination of ordered_ab_semigroup_add + 1.78 -comm_monoid_add. INCOMPATIBILITY. 1.79 - 1.80 -* Introduced the type classes canonically_ordered_comm_monoid_add and 1.81 -dioid. 1.82 - 1.83 -* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 1.84 -instantiating linordered_semiring_strict and ordered_ab_group_add, an 1.85 -explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 1.86 -be required. INCOMPATIBILITY. 1.87 - 1.88 * HOL-Library: multisets are now ordered with the multiset ordering 1.89 #\<subseteq># ~> \<le> 1.90 #\<subset># ~> < 1.91 @@ -886,7 +875,7 @@ 1.92 empty_inter [simp] ~> [] 1.93 INCOMPATIBILITY. 1.94 1.95 -* Session HOL-Library, theory Multiset: The order of the variables in 1.96 +* Session HOL-Library, theory Multiset: the order of the variables in 1.97 the second cases of multiset_induct, multiset_induct2_size, 1.98 multiset_induct2 has been changed (e.g. Add A a ~> Add a A). 1.99 INCOMPATIBILITY. 1.100 @@ -933,6 +922,16 @@ 1.101 1.102 Added theory of longest common prefixes. 1.103 1.104 +* Session HOL-Number_Theory: algebraic foundation for primes: 1.105 +Generalisation of predicate "prime" and introduction of predicates 1.106 +"prime_elem", "irreducible", a "prime_factorization" function, and the 1.107 +"factorial_ring" typeclass with instance proofs for nat, int, poly. Some 1.108 +theorems now have different names, most notably "prime_def" is now 1.109 +"prime_nat_iff". INCOMPATIBILITY. 1.110 + 1.111 +* Session Old_Number_Theory has been removed, after porting remaining 1.112 +theories. 1.113 + 1.114 1.115 *** ML *** 1.116