src/HOL/Number_Theory/Primes.thy
changeset 47108 2a1953f0d20d
parent 45605 a89b4bc311a5
child 53598 2bd8d459ebae
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -206,7 +206,7 @@
     1.4      "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
     1.5    by (auto simp add: prime_nat_code)
     1.6  
     1.7 -lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m"] for m
     1.8 +lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
     1.9  
    1.10  lemma prime_int_code [code]:
    1.11    "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
    1.12 @@ -222,7 +222,7 @@
    1.13  lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
    1.14    by (auto simp add: prime_int_code)
    1.15  
    1.16 -lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m"] for m
    1.17 +lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
    1.18  
    1.19  lemma two_is_prime_nat [simp]: "prime (2::nat)"
    1.20    by simp