--- a/src/HOL/NumberTheory/Fib.thy Tue Oct 03 22:36:22 2000 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Tue Oct 03 22:37:16 2000 +0200
@@ -6,7 +6,7 @@
The Fibonacci function. Demonstrates the use of recdef.
*)
-Fib = Divides + Primes +
+Fib = Primes +
consts fib :: "nat => nat"
recdef fib "less_than"