dropped warnings by dropping ineffective code declarations
authorhaftmann
Fri Jun 12 08:53:23 2015 +0200 (2015-06-12)
changeset 60431db9c67b760f1
parent 60430 ce559c850a27
child 60432 68d75cff8809
dropped warnings by dropping ineffective code declarations
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -1478,7 +1478,7 @@
     1.4    by (induct rule: finite.induct[OF `finite A`])
     1.5      (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
     1.6  
     1.7 -lemma Lcm_set [code, code_unfold]:
     1.8 +lemma Lcm_set [code_unfold]:
     1.9    "Lcm (set xs) = fold lcm xs 1"
    1.10    using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite by (simp add: ac_simps)
    1.11  
    1.12 @@ -1571,7 +1571,7 @@
    1.13    by (induct rule: finite.induct[OF `finite A`])
    1.14      (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
    1.15  
    1.16 -lemma Gcd_set [code, code_unfold]:
    1.17 +lemma Gcd_set [code_unfold]:
    1.18    "Gcd (set xs) = fold gcd xs 0"
    1.19    using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps)
    1.20