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 57512 cc97b347b301
parent 55656 eb07b0acbebc
child 58614 7338eb25226c 
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -92,7 +92,7 @@
 proof -
   assume "0 < n"
   then have "gcd (n * k + m) n = gcd n (m mod n)"
-    by (simp add: gcd_non_0_nat add_commute)
+    by (simp add: gcd_non_0_nat add.commute)
   also from `0 < n` have "\<dots> = gcd m n"
     by (simp add: gcd_non_0_nat)
   finally show ?thesis .
isabelle