# HG changeset patch
# User haftmann
# Date 1762109250 -3600
# Node ID d7c525fd68b27fb14d9c2c4080b48c4162f6bda8
# Parent  644145d9d022649ed9ecc707f9dbf7517abd96bf
avoid computation checks when using theories as regular libraries

diff -r 644145d9d022 -r d7c525fd68b2 src/HOL/Computational_Algebra/Computation_Checks.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Computational_Algebra/Computation_Checks.thy	Sun Nov 02 19:47:30 2025 +0100
@@ -0,0 +1,28 @@
+(*  Title:      HOL/Computational_Algebra/Computation_Checks.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Computation checks\<close>
+
+theory Computation_Checks
+imports Primes Polynomial_Factorial
+begin
+
+text \<open>
+  @{lemma \<open>prime (997::nat)\<close> by eval}
+\<close>
+
+text \<open>
+  @{lemma \<open>prime (997::int)\<close> by eval}
+\<close>
+
+text \<open>
+  @{lemma \<open>Gcd {[:1, 2, 3:], [:2, 3, (4 :: int):]} = 1\<close> by eval}
+\<close>
+
+text \<open>
+  @{lemma \<open>Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]\<close> by eval}
+\<close>
+
+end
+
diff -r 644145d9d022 -r d7c525fd68b2 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sat Nov 01 12:50:07 2025 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Nov 02 19:47:30 2025 +0100
@@ -750,8 +750,4 @@
 lemmas Lcm_poly_set_eq_fold [code] =
   Lcm_set_eq_fold [where ?'a = "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"]
 
-text \<open>Example:
-  @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
-\<close>
-  
 end
diff -r 644145d9d022 -r d7c525fd68b2 src/HOL/Computational_Algebra/Primes.thy
--- 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
diff -r 644145d9d022 -r d7c525fd68b2 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Nov 01 12:50:07 2025 +0000
+++ b/src/HOL/ROOT	Sun Nov 02 19:47:30 2025 +0100
@@ -152,6 +152,8 @@
     Computational_Algebra
     (*conflicting type class instantiations and dependent applications*)
     Field_as_Ring
+    (*checks that computation works*)
+    Computation_Checks
   document_files
     "root.tex"
     "root.bib"