diff options
Diffstat (limited to 'etc/isa/depends/Fib.thy')
-rw-r--r-- | etc/isa/depends/Fib.thy | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/etc/isa/depends/Fib.thy b/etc/isa/depends/Fib.thy deleted file mode 100644 index 9272ed8c..00000000 --- a/etc/isa/depends/Fib.thy +++ /dev/null @@ -1,17 +0,0 @@ -(* 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 = Usedepends + Divides + Primes + - -consts fib :: "nat => nat" -recdef fib "less_than" - zero "fib 0 = 0" - one "fib 1 = 1" - Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)" - -end |