src/HOL/Library/Primes.thy
changeset 23839 d9fa0f457d9a
parent 22665 cf152ff55d16
child 25593 0b0df6c8646a
     1.1 --- a/src/HOL/Library/Primes.thy	Tue Jul 17 22:51:27 2007 +0200
     1.2 +++ b/src/HOL/Library/Primes.thy	Wed Jul 18 11:43:06 2007 +0200
     1.3 @@ -27,10 +27,7 @@
     1.4  
     1.5  lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
     1.6    apply (auto simp add: prime_def)
     1.7 -  apply (drule_tac x = "gcd (p, n)" in spec)
     1.8 -  apply auto
     1.9 -  apply (insert gcd_dvd2 [of p n])
    1.10 -  apply simp
    1.11 +  apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
    1.12    done
    1.13  
    1.14  text {*