src/HOL/Library/Polynomial_Factorial.thy
changeset 64850 fc9265882329
parent 64848 c50db2128048
child 64860 4d56170d97b3
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 18:53:20 2017 +0100
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 19:13:49 2017 +0100
     1.3 @@ -981,12 +981,9 @@
     1.4    shows "lcm p q = normalize (p * q) div gcd p q"
     1.5    by (fact lcm_gcd)
     1.6  
     1.7 -declare Gcd_set
     1.8 -  [where ?'a = "'a :: factorial_ring_gcd poly", code]
     1.9 -
    1.10 -declare Lcm_set
    1.11 -  [where ?'a = "'a :: factorial_ring_gcd poly", code]
    1.12 -
    1.13 +lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
    1.14 +lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
    1.15 +  
    1.16  text \<open>Example:
    1.17    @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
    1.18  \<close>