Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Number_Theory/Fib.thy
changeset 60688 01488b559910
parent 60527 eb431a5651fe
child 61649 268d88ec9087 
--- a/src/HOL/Number_Theory/Fib.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -67,7 +67,7 @@
   apply (cases m)
   apply (auto simp add: fib_add)
   apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
-    gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
+    gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute)
   done
 
 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
isabelle