Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned deps;
authorwenzelm
Tue, 03 Oct 2000 22:37:16 +0200
changeset 10147 178deaacb244
parent 10146 e89309dde9d3
child 10148 739327964a5c
tuned deps;
src/HOL/NumberTheory/Fib.thy file | annotate | diff | comparison | revisions
src/HOL/NumberTheory/IntPrimes.thy file | annotate | diff | comparison | revisions 
--- 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"
--- a/src/HOL/NumberTheory/IntPrimes.thy	Tue Oct 03 22:36:22 2000 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Oct 03 22:37:16 2000 +0200
@@ -4,7 +4,7 @@
     Copyright	2000  University of Cambridge
 *)
 
-IntPrimes = Main + IntDiv + Primes +
+IntPrimes = Primes +
 
 consts
   xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
isabelle