src/HOL/NumberTheory/Fib.thy
changeset 10147 178deaacb244
parent 9944 2a705d1af4dc
child 11049 7eef34adb852
     1.1 --- a/src/HOL/NumberTheory/Fib.thy	Tue Oct 03 22:36:22 2000 +0200
     1.2 +++ b/src/HOL/NumberTheory/Fib.thy	Tue Oct 03 22:37:16 2000 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  The Fibonacci function.  Demonstrates the use of recdef.
     1.5  *)
     1.6  
     1.7 -Fib = Divides + Primes +
     1.8 +Fib = Primes +
     1.9  
    1.10  consts fib  :: "nat => nat"
    1.11  recdef fib "less_than"