src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 64850 fc9265882329
parent 64848 c50db2128048
child 64911 f0e07600de47
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 18:53:20 2017 +0100
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 19:13:49 2017 +0100
     1.3 @@ -254,12 +254,12 @@
     1.4  qed
     1.5  
     1.6  lemma Gcd_eucl_set [code]:
     1.7 -  "Gcd (set xs) = foldl gcd 0 xs"
     1.8 -  by (fact local.Gcd_set)
     1.9 +  "Gcd (set xs) = fold gcd xs 0"
    1.10 +  by (fact Gcd_set_eq_fold)
    1.11  
    1.12  lemma Lcm_eucl_set [code]:
    1.13 -  "Lcm (set xs) = foldl lcm 1 xs"
    1.14 -  by (fact local.Lcm_set)
    1.15 +  "Lcm (set xs) = fold lcm xs 1"
    1.16 +  by (fact Lcm_set_eq_fold)
    1.17   
    1.18  end
    1.19