tuned NEWS
authorhaftmann
Wed Jan 04 21:28:33 2017 +0100 (2017-01-04)
changeset 64787067cacdd1117
parent 64786 340db65fd2c1
child 64788 19f3d4af7a7d
child 64796 22a1b061ae15
tuned NEWS
NEWS
     1.1 --- a/NEWS	Wed Jan 04 21:28:29 2017 +0100
     1.2 +++ b/NEWS	Wed Jan 04 21:28:33 2017 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -* Dropped abbreviation transP, antisymP, single_valuedP;
     1.8 +* Dropped abbreviations transP, antisymP, single_valuedP;
     1.9  use constants transp, antisymp, single_valuedp instead.
    1.10  INCOMPATIBILITY.
    1.11  
    1.12 @@ -37,6 +37,10 @@
    1.13      available as "bezout_coefficients".
    1.14  INCOMPATIBILITY.
    1.15  
    1.16 +* Named collection mod_simps covers various congruence rules
    1.17 +concerning mod, replacing former zmod_simps.
    1.18 +INCOMPATIBILITY.
    1.19 +
    1.20  * Swapped orientation of congruence rules mod_add_left_eq,
    1.21  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.22  mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
    1.23 @@ -49,10 +53,6 @@
    1.24      zmod_eq_dvd_iff ~> mod_eq_dvd_iff
    1.25  INCOMPATIBILITY.
    1.26  
    1.27 -* Named collection mod_simps covers various congruence rules
    1.28 -concerning mod, replacing former zmod_simps.
    1.29 -INCOMPATIBILITY.
    1.30 -
    1.31  * (Co)datatype package:
    1.32    - The 'size_gen_o_map' lemma is no longer generated for datatypes
    1.33      with type class annotations. As a result, the tactic that derives