NEWS
changeset 64391 553d8c4d7ef4
parent 64390 ad2c5f37f659
child 64439 2bafda87b524
child 64457 f7aa4d0f7d02
     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