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/Isar_Examples/Fibonacci.thy
changeset 62429 25271ff79171
parent 62348 9a5f43dac883
child 63095 201480e65b7d 
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Fri Feb 26 18:33:01 2016 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Fri Feb 26 22:15:09 2016 +0100
@@ -80,7 +80,7 @@
   also have "\<dots> = fib (n + 2) + fib (n + 1)"
     by simp
   also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
-    by (rule gcd_add2_nat)
+    by (rule gcd_add2)
   also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
     by (simp add: gcd.commute)
   also assume "\<dots> = 1"
isabelle