src/HOL/GCD.thy
changeset 54437 0060957404c7
parent 54257 5c7a3b6b05a9
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/GCD.thy	Sat Nov 16 07:45:53 2013 +0100
     1.2 +++ b/src/HOL/GCD.thy	Fri Nov 15 22:02:01 2013 +0100
     1.3 @@ -1654,11 +1654,11 @@
     1.4  apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
     1.5  done
     1.6  
     1.7 -lemma Lcm_set_nat [code_unfold]:
     1.8 +lemma Lcm_set_nat [code, code_unfold]:
     1.9    "Lcm (set ns) = fold lcm ns (1::nat)"
    1.10    by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
    1.11  
    1.12 -lemma Gcd_set_nat [code_unfold]:
    1.13 +lemma Gcd_set_nat [code, code_unfold]:
    1.14    "Gcd (set ns) = fold gcd ns (0::nat)"
    1.15    by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
    1.16  
    1.17 @@ -1730,11 +1730,11 @@
    1.18    assumes "\<forall>m\<in>M. n dvd m" shows "n dvd Gcd M"
    1.19    using assms by (simp add: Gcd_int_def dvd_int_iff)
    1.20  
    1.21 -lemma Lcm_set_int [code_unfold]:
    1.22 +lemma Lcm_set_int [code, code_unfold]:
    1.23    "Lcm (set xs) = fold lcm xs (1::int)"
    1.24    by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
    1.25  
    1.26 -lemma Gcd_set_int [code_unfold]:
    1.27 +lemma Gcd_set_int [code, code_unfold]:
    1.28    "Gcd (set xs) = fold gcd xs (0::int)"
    1.29    by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
    1.30