--- a/src/HOL/Isar_examples/Fibonacci.thy Thu Jun 26 10:06:51 2008 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Thu Jun 26 10:06:53 2008 +0200
@@ -15,7 +15,9 @@
header {* Fib and Gcd commute *}
-theory Fibonacci imports Primes begin
+theory Fibonacci
+imports Primes
+begin
text_raw {*
\footnote{Isar version by Gertrud Bauer. Original tactic script by
@@ -26,11 +28,10 @@
subsection {* Fibonacci numbers *}
-consts fib :: "nat => nat"
-recdef fib less_than
+fun fib :: "nat \<Rightarrow> nat" where
"fib 0 = 0"
- "fib (Suc 0) = 1"
- "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+ | "fib (Suc 0) = 1"
+ | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "0 < fib (Suc n)"
by (induct n rule: fib.induct) simp_all