src/HOL/Number_Theory/Primes.thy
changeset 63635 858a225ebb62
parent 63633 2accfb71e33b
child 63766 695d60817cb1
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Aug 09 11:57:24 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Aug 09 12:30:31 2016 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4  
     1.5  lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
     1.6  
     1.7 -lemma two_prime_nat [simp]: "prime (2::nat)"
     1.8 +lemma two_is_prime_nat [simp]: "prime (2::nat)"
     1.9    by simp
    1.10  
    1.11  declare prime_int_nat_transfer[of "numeral m" for m, simp]
    1.12 @@ -615,4 +615,4 @@
    1.13  lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
    1.14  lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end