aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isa/depends/Fib.thy
diff options
context:
space:
mode:
Diffstat (limited to 'etc/isa/depends/Fib.thy')
-rw-r--r--etc/isa/depends/Fib.thy17
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