src/HOL/Number_Theory/Primes.thy
changeset 54228 229282d53781
parent 53598 2bd8d459ebae
child 55130 70db8d380d62
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -74,8 +74,9 @@
     1.4  subsection {* Primes *}
     1.5  
     1.6  lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
     1.7 -  unfolding prime_nat_def
     1.8 -  by (metis gcd_lcm_complete_lattice_nat.bot_least nat_even_iff_2_dvd nat_neq_iff odd_1_nat)
     1.9 +  apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
    1.10 +  apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
    1.11 +  done
    1.12  
    1.13  lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    1.14    unfolding prime_int_def