src/HOL/Computational_Algebra/Primes.thy
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