src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Mon Feb 16 19:35:52 2009 -0800
+++ b/src/HOL/Divides.thy	Tue Feb 17 18:48:17 2009 +0100
@@ -173,7 +173,7 @@
 qed
 
 lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
-by (unfold dvd_def, auto)
+by (rule dvd_eq_mod_eq_0[THEN iffD1])
 
 lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
 by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)