src/HOL/Number_Theory/Eratosthenes.thy
changeset 63633 2accfb71e33b
parent 63534 523b488b15c9
child 64243 aee949f6642d
     1.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Mon Aug 08 14:13:14 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Mon Aug 08 17:47:51 2016 +0200
     1.3 @@ -295,8 +295,8 @@
     1.4      from 2 show ?thesis
     1.5        apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
     1.6          dest: prime_gt_Suc_0_nat)
     1.7 -      apply (metis One_nat_def Suc_le_eq less_not_refl is_prime_nat_iff)
     1.8 -      apply (metis One_nat_def Suc_le_eq aux is_prime_nat_iff)
     1.9 +      apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_iff)
    1.10 +      apply (metis One_nat_def Suc_le_eq aux prime_nat_iff)
    1.11        done
    1.12    qed
    1.13  qed