diff -r 0929d6d08dd3 -r a52309ac4a4d src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Tue Jan 22 23:06:58 2008 +0100
+++ b/src/HOL/IntDiv.thy	Tue Jan 22 23:07:21 2008 +0100
@@ -712,6 +712,7 @@
 apply (erule subst, simp_all)
 done
 
+
 subsection{*More Algebraic Laws for div and mod*}
 
 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
@@ -746,6 +747,9 @@
 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
 by (simp add: zdiv_zmult1_eq)
 
+instance int :: semiring_div
+  by intro_classes auto
+
 lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
 by (subst mult_commute, erule zdiv_zmult_self1)
 
@@ -1053,7 +1057,6 @@
        simp) 
 done
 
-
 (*Not clear why this must be proved separately; probably number_of causes
   simplification problems*)
 lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
@@ -1152,9 +1155,6 @@
 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   by (simp add: dvd_def zmod_eq_0_iff)
 
-instance int :: dvd_mod
-  by default (simp add: 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]