changeset 10795 | 9e888d60d3e5 |
parent 10790 | 520dd8696927 |
child 10846 | 623141a08705 |
--- a/doc-src/TutorialI/Rules/Primes.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Rules/Primes.thy Fri Jan 05 18:32:57 2001 +0100 @@ -84,7 +84,7 @@ done; theorem gcd_greatest_iff [iff]: - "k dvd gcd(m,n) = (k dvd m \<and> k dvd n)" + "(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)" apply (blast intro!: gcd_greatest intro: dvd_trans); done;