--- a/NEWS Wed Jan 04 21:28:29 2017 +0100
+++ b/NEWS Wed Jan 04 21:28:33 2017 +0100
@@ -19,7 +19,7 @@
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
INCOMPATIBILITY.
-* Dropped abbreviation transP, antisymP, single_valuedP;
+* Dropped abbreviations transP, antisymP, single_valuedP;
use constants transp, antisymp, single_valuedp instead.
INCOMPATIBILITY.
@@ -37,6 +37,10 @@
available as "bezout_coefficients".
INCOMPATIBILITY.
+* Named collection mod_simps covers various congruence rules
+concerning mod, replacing former zmod_simps.
+INCOMPATIBILITY.
+
* Swapped orientation of congruence rules mod_add_left_eq,
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
@@ -49,10 +53,6 @@
zmod_eq_dvd_iff ~> mod_eq_dvd_iff
INCOMPATIBILITY.
-* Named collection mod_simps covers various congruence rules
-concerning mod, replacing former zmod_simps.
-INCOMPATIBILITY.
-
* (Co)datatype package:
- The 'size_gen_o_map' lemma is no longer generated for datatypes
with type class annotations. As a result, the tactic that derives