NEWS
changeset 68157 057d5b4ce47e
parent 68125 2e5b737810a6
child 68200 5859c688102a
     1.1 --- a/NEWS	Sat May 12 17:53:12 2018 +0200
     1.2 +++ b/NEWS	Sat May 12 22:20:46 2018 +0200
     1.3 @@ -328,6 +328,15 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Eliminated some theorem duplicate variations:
     1.8 +  * dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0.
     1.9 +  * mod_Suc_eq_Suc_mod can be replaced by mod_Suc.
    1.10 +  * mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps.
    1.11 +  * mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def.
    1.12 +  * The witness of mod_eqD can be given directly as "_ div _".
    1.13 +
    1.14 +INCOMPATIBILITY.
    1.15 +
    1.16  
    1.17  *** ML ***
    1.18