1.1 --- a/NEWS	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/NEWS	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -376,12 +376,16 @@
     1.4      mult_div ~>             div_mult_self2_is_id
     1.5      mult_mod ~>             mod_mult_self2_is_0
     1.6  
     1.7 -* HOL/IntDiv: removed most (all?) lemmas that are instances of class-based
     1.8 +* HOL/IntDiv: removed many lemmas that are instances of class-based
     1.9  generalizations (from Divides and Ring_and_Field).
    1.10  INCOMPATIBILITY. Rename old lemmas as follows:
    1.11  
    1.12  dvd_diff               -> nat_dvd_diff
    1.13  dvd_zminus_iff         -> dvd_minus_iff
    1.14 +mod_add1_eq            -> mod_add_eq
    1.15 +mod_mult1_eq           -> mod_mult_right_eq
    1.16 +mod_mult1_eq'          -> mod_mult_left_eq
    1.17 +mod_mult_distrib_mod   -> mod_mult_eq
    1.18  nat_mod_add_left_eq    -> mod_add_left_eq
    1.19  nat_mod_add_right_eq   -> mod_add_right_eq
    1.20  nat_mod_div_trivial    -> mod_div_trivial
    1.21 @@ -398,7 +402,7 @@
    1.22  zmod_zadd_right_eq     -> mod_add_right_eq
    1.23  zmod_zadd_self1        -> mod_add_self1
    1.24  zmod_zadd_self2        -> mod_add_self2
    1.25 -zmod_zadd1_eq          -> mod_add1_eq
    1.26 +zmod_zadd1_eq          -> mod_add_eq
    1.27  zmod_zdiff1_eq         -> mod_diff_eq
    1.28  zmod_zdvd_zmod         -> mod_mod_cancel
    1.29  zmod_zmod_cancel       -> mod_mod_cancel