src/HOL/Number_Theory/Primes.thy
changeset 59730 b7c394c7a619
parent 59669 de7792ea4090
child 60526 fad653acf58f
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 16:12:35 2015 +0000
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Mar 16 15:30:00 2015 +0000
     1.3 @@ -226,7 +226,7 @@
     1.4  
     1.5  lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
     1.6  proof-
     1.7 -  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
     1.8 +  have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
     1.9    from prime_factor_nat [OF f1]
    1.10    obtain p where "prime p" and "p dvd fact n + 1" by auto
    1.11    then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
    1.12 @@ -234,7 +234,7 @@
    1.13      from `prime p` have "p \<ge> 1"
    1.14        by (cases p, simp_all)
    1.15      with `p <= n` have "p dvd fact n"
    1.16 -      by (intro dvd_fact_nat)
    1.17 +      by (intro dvd_fact)
    1.18      with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
    1.19        by (rule dvd_diff_nat)
    1.20      then have "p dvd 1" by simp