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