src/HOL/Presburger.thy
changeset 30031 bd786c37af84
parent 30027 ab40c5e007e0
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Presburger.thy	Fri Feb 20 21:29:34 2009 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Fri Feb 20 23:46:03 2009 +0100
     1.3 @@ -412,14 +412,10 @@
     1.4    "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
     1.5    by (rule eq_number_of_eq)
     1.6  
     1.7 -lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
     1.8 -unfolding dvd_eq_mod_eq_0[symmetric] ..
     1.9 -
    1.10 -lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
    1.11 -unfolding zdvd_iff_zmod_eq_0[symmetric] ..
    1.12 +declare dvd_eq_mod_eq_0[symmetric, presburger]
    1.13  declare mod_1[presburger] 
    1.14  declare mod_0[presburger]
    1.15 -declare zmod_1[presburger]
    1.16 +declare mod_by_1[presburger]
    1.17  declare zmod_zero[presburger]
    1.18  declare zmod_self[presburger]
    1.19  declare mod_self[presburger]