| changeset 83357 | d7c525fd68b2 |
| parent 82518 | da14e77a48b2 |
| child 83358 | 1cf4f1e930af |
--- a/src/HOL/Computational_Algebra/Primes.thy Sat Nov 01 12:50:07 2025 +0000 +++ b/src/HOL/Computational_Algebra/Primes.thy Sun Nov 02 19:47:30 2025 +0100 @@ -1079,10 +1079,6 @@ "prime_int p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)" by (auto simp add: prime_int_iff') -lemma "prime(997::nat)" by eval - -lemma "prime(997::int)" by eval - end end