tuned deps;
authorwenzelm
Tue Oct 03 22:37:16 2000 +0200 (2000-10-03)
changeset 10147178deaacb244
parent 10146 e89309dde9d3
child 10148 739327964a5c
tuned deps;
src/HOL/NumberTheory/Fib.thy
src/HOL/NumberTheory/IntPrimes.thy
     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"
     2.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Tue Oct 03 22:36:22 2000 +0200
     2.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Oct 03 22:37:16 2000 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4      Copyright	2000  University of Cambridge
     2.5  *)
     2.6  
     2.7 -IntPrimes = Main + IntDiv + Primes +
     2.8 +IntPrimes = Primes +
     2.9  
    2.10  consts
    2.11    xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"