src/HOL/ex/Fib.thy

New record type of programs

(*  Title:      ex/Fib
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1997  University of Cambridge

The Fibonacci function.  Demonstrates the use of recdef.
*)

Fib = WF_Rel + Divides + Primes +

consts fib  :: "nat => nat"
recdef fib "less_than"
    "fib 0 = 0"
    "fib 1 = 1"
    "fib (Suc(Suc x)) = (fib x + fib (Suc x))"

end