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