src/HOL/Isar_examples/Fibonacci.thy
changeset 11464 ddea204de5bc
parent 10408 d8b3613158b1
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  consts fib :: "nat => nat"
     1.5  recdef fib less_than
     1.6   "fib 0 = 0"
     1.7 - "fib 1 = 1"
     1.8 + "fib 1' = 1"
     1.9   "fib (Suc (Suc x)) = fib x + fib (Suc x)"
    1.10  
    1.11  lemma [simp]: "0 < fib (Suc n)"