src/HOL/Isar_Examples/Fibonacci.thy
changeset 61799 4cf66f21b764
parent 58882 6e2010ab8bd9
child 61932 2e48182cc82c
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -52,7 +52,7 @@
 lemma fib_add:
   "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
   (is "?P n")
-  -- \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
+  \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
 proof (induct n rule: fib_induct)
   show "?P 0" by simp
   show "?P 1" by simp