doc-src/TutorialI/Rules/Forward.thy

--- a/doc-src/TutorialI/Rules/Forward.thy	Sun Jul 20 11:10:04 2008 +0200
+++ b/doc-src/TutorialI/Rules/Forward.thy	Sun Jul 20 11:19:08 2008 +0200
@@ -192,8 +192,7 @@
 *)
 
 lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
-by (blast intro: relprime_dvd_mult dvd_trans)
-
+by (auto intro: relprime_dvd_mult elim: dvdE)
 
 lemma relprime_20_81: "gcd 20 81 = 1";
 by (simp add: gcd.simps)