src/HOL/Number_Theory/Fib.thy
changeset 60688 01488b559910
parent 60527 eb431a5651fe
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Wed Jul 08 14:01:40 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Wed Jul 08 14:01:41 2015 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4    apply (cases m)
     1.5    apply (auto simp add: fib_add)
     1.6    apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
     1.7 -    gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
     1.8 +    gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute)
     1.9    done
    1.10  
    1.11  lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"