src/HOL/Number_Theory/Fib.thy
changeset 57512 cc97b347b301
parent 54713 6666fc0b9ebc
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
     1.5    apply (induct n rule: fib.induct)
     1.6    apply auto
     1.7 -  apply (metis gcd_add1_nat nat_add_commute)
     1.8 +  apply (metis gcd_add1_nat add.commute)
     1.9    done
    1.10  
    1.11  lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
    1.12 @@ -68,7 +68,7 @@
    1.13    apply (cases m)
    1.14    apply (auto simp add: fib_add)
    1.15    apply (subst gcd_commute_nat)
    1.16 -  apply (subst mult_commute)
    1.17 +  apply (subst mult.commute)
    1.18    apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
    1.19    done
    1.20