equal
deleted
inserted
replaced
241 "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" |
241 "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" |
242 by (auto simp add: prime_int_code) |
242 by (auto simp add: prime_int_code) |
243 |
243 |
244 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m |
244 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m |
245 |
245 |
246 lemma two_prime_nat [simp]: "prime (2::nat)" |
246 lemma two_is_prime_nat [simp]: "prime (2::nat)" |
247 by simp |
247 by simp |
248 |
248 |
249 declare prime_int_nat_transfer[of "numeral m" for m, simp] |
249 declare prime_int_nat_transfer[of "numeral m" for m, simp] |
250 |
250 |
251 |
251 |