src/HOL/Library/Primes.thy
changeset 13187 e5434b822a96
parent 13032 1ec445c51931
child 14353 79f9fbef9106
     1.1 --- a/src/HOL/Library/Primes.thy	Thu May 30 10:12:11 2002 +0200
     1.2 +++ b/src/HOL/Library/Primes.thy	Thu May 30 10:12:52 2002 +0200
     1.3 @@ -185,7 +185,6 @@
     1.4    apply (auto simp add: prime_def)
     1.5    apply (case_tac m)
     1.6     apply (auto dest!: dvd_imp_le)
     1.7 -  apply arith
     1.8    done
     1.9  
    1.10  text {*