src/HOL/NumberTheory/Fib.thy
changeset 10147 178deaacb244
parent 9944 2a705d1af4dc
child 11049 7eef34adb852
equal deleted inserted replaced
10146:e89309dde9d3 10147:178deaacb244
     4     Copyright   1997  University of Cambridge
     4     Copyright   1997  University of Cambridge
     5 
     5 
     6 The Fibonacci function.  Demonstrates the use of recdef.
     6 The Fibonacci function.  Demonstrates the use of recdef.
     7 *)
     7 *)
     8 
     8 
     9 Fib = Divides + Primes +
     9 Fib = Primes +
    10 
    10 
    11 consts fib  :: "nat => nat"
    11 consts fib  :: "nat => nat"
    12 recdef fib "less_than"
    12 recdef fib "less_than"
    13   zero    "fib 0 = 0"
    13   zero    "fib 0 = 0"
    14   one     "fib 1 = 1"
    14   one     "fib 1 = 1"