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