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