src/HOL/IntDiv.thy
changeset 23684 8c508c4dc53b
parent 23512 770e7f9f715b
child 23853 2c69bb1374b8
--- a/src/HOL/IntDiv.thy	Tue Jul 10 00:43:51 2007 +0200
+++ b/src/HOL/IntDiv.thy	Tue Jul 10 09:23:10 2007 +0200
@@ -1064,13 +1064,8 @@
 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   by (simp add: dvd_def zmod_eq_0_iff)
 
-definition
-  dvd_int :: "int \<Rightarrow> int \<Rightarrow> bool"
-where
-  "dvd_int = op dvd"
-
-lemmas [code inline] = dvd_int_def [symmetric]
-lemmas [code, folded dvd_int_def, code func] = zdvd_iff_zmod_eq_0
+instance int :: dvd_mod
+  by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0)
 
 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]