changeset 27657 | 0efc8b68ee4a |
parent 25261 | 3dc292be0b54 |
child 33750 | 0a0d6d79d984 |
--- 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*)