| changeset 50037 | f2a32197a33a |
| parent 41541 | 1fa4725c4656 |
| child 53015 | a1119cf551e8 |
--- a/src/HOL/Old_Number_Theory/Primes.thy Thu Nov 08 19:55:37 2012 +0100 +++ b/src/HOL/Old_Number_Theory/Primes.thy Thu Nov 08 20:02:41 2012 +0100 @@ -24,7 +24,7 @@ lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd p n = 1" apply (auto simp add: prime_def) - apply (metis One_nat_def gcd_dvd1 gcd_dvd2) + apply (metis gcd_dvd1 gcd_dvd2) done text {*