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
```