# HG changeset patch
# User haftmann
# Date 1216545004 -7200
# Node ID 0efc8b68ee4ab18d272ba29329835d650310bd03
# Parent  d4f6e64ee7ccef5895e1b2c4e27cf84c14aa201b
(adjusted)

diff -r d4f6e64ee7cc -r 0efc8b68ee4a doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Sat Jul 19 19:27:13 2008 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Sun Jul 20 11:10:04 2008 +0200
@@ -151,7 +151,7 @@
 
 
 lemma gcd_dvd_gcd_mult: "gcd m n dvd gcd (k*m) n"
-  apply (blast intro: dvd_trans);
+  apply (auto intro: dvd_trans [of _ m])
   done
 
 (*This is half of the proof (by dvd_anti_sym) of*)