# HG changeset patch
# User wenzelm
# Date 1477390457 -7200
# Node ID 553d8c4d7ef444885ec1a668415662ea0a48e1ec
# Parent  ad2c5f37f6590e1d261d0ec32298af95500e8534
tuned;

diff -r ad2c5f37f659 -r 553d8c4d7ef4 NEWS
--- 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 ***