1.1 --- a/src/HOL/Presburger.thy	Tue Mar 27 16:04:51 2012 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Tue Mar 27 19:21:05 2012 +0200
     1.3 @@ -405,8 +405,8 @@
     1.4  declare mod_div_equality[presburger]
     1.5  declare mod_mult_self1[presburger]
     1.6  declare mod_mult_self2[presburger]
     1.7 -declare zdiv_zmod_equality2[presburger]
     1.8 -declare zdiv_zmod_equality[presburger]
     1.9 +declare div_mod_equality[presburger]
    1.10 +declare div_mod_equality2[presburger]
    1.11  declare mod2_Suc_Suc[presburger]
    1.12  lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
    1.13  by simp_all