tuned code setup
authorhaftmann
Sat Jun 27 20:20:33 2015 +0200 (2015-06-27)
changeset 605972da9b632069b
parent 60596 54168997757f
child 60598 78ca5674c66a
tuned code setup
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Sat Jun 27 20:20:32 2015 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sat Jun 27 20:20:33 2015 +0200
     1.3 @@ -1510,6 +1510,10 @@
     1.4    "Gcd {} = 0"
     1.5    by (rule dvd_0_left, rule dvd_Gcd) simp
     1.6  
     1.7 +lemma Gcd_set [code_unfold]:
     1.8 +  "Gcd (set as) = foldr gcd as 0"
     1.9 +  by (induct as) simp_all
    1.10 +  
    1.11  end
    1.12  
    1.13  lemma dvd_Lcm_nat [simp]:
    1.14 @@ -1643,7 +1647,7 @@
    1.15    "Lcm (set ns) = fold lcm ns (1::nat)"
    1.16    by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
    1.17  
    1.18 -lemma Gcd_set_nat [code, code_unfold]:
    1.19 +lemma Gcd_set_nat [code]:
    1.20    "Gcd (set ns) = fold gcd ns (0::nat)"
    1.21    by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
    1.22  
    1.23 @@ -1706,7 +1710,7 @@
    1.24    "Lcm (set xs) = fold lcm xs (1::int)"
    1.25    by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
    1.26  
    1.27 -lemma Gcd_set_int [code, code_unfold]:
    1.28 +lemma Gcd_set_int [code]:
    1.29    "Gcd (set xs) = fold gcd xs (0::int)"
    1.30    by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
    1.31