# HG changeset patch
# User haftmann
# Date 1483561713 -3600
# Node ID 067cacdd1117665d612af8e1a4ec70469dbfc4bb
# Parent  340db65fd2c1d87ea110392e3a54f7fd7832a7c6
tuned NEWS

diff -r 340db65fd2c1 -r 067cacdd1117 NEWS
--- 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