1.1 --- a/src/HOL/IntDiv.thy	Tue Jul 10 00:43:51 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 10 09:23:10 2007 +0200
     1.3 @@ -1064,13 +1064,8 @@
     1.4  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
     1.5    by (simp add: dvd_def zmod_eq_0_iff)
     1.6  
     1.7 -definition
     1.8 -  dvd_int :: "int \<Rightarrow> int \<Rightarrow> bool"
     1.9 -where
    1.10 -  "dvd_int = op dvd"
    1.11 -
    1.12 -lemmas [code inline] = dvd_int_def [symmetric]
    1.13 -lemmas [code, folded dvd_int_def, code func] = zdvd_iff_zmod_eq_0
    1.14 +instance int :: dvd_mod
    1.15 +  by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0)
    1.16  
    1.17  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    1.18    zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]