src/HOL/Library/Polynomial_Factorial.thy
changeset 64860 4d56170d97b3
parent 64850 fc9265882329
child 64911 f0e07600de47
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 23:27:10 2017 +0100
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 23:00:11 2017 +0100
     1.3 @@ -983,7 +983,7 @@
     1.4  
     1.5  lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
     1.6  lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
     1.7 -  
     1.8 +
     1.9  text \<open>Example:
    1.10    @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
    1.11  \<close>