diff -r de51a86fc903 -r cc97b347b301 src/HOL/Number_Theory/Fib.thy --- a/src/HOL/Number_Theory/Fib.thy Fri Jul 04 20:07:08 2014 +0200 +++ b/src/HOL/Number_Theory/Fib.thy Fri Jul 04 20:18:47 2014 +0200 @@ -60,7 +60,7 @@ lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))" apply (induct n rule: fib.induct) apply auto - apply (metis gcd_add1_nat nat_add_commute) + apply (metis gcd_add1_nat add.commute) done lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" @@ -68,7 +68,7 @@ apply (cases m) apply (auto simp add: fib_add) apply (subst gcd_commute_nat) - apply (subst mult_commute) + apply (subst mult.commute) apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute) done