--- a/src/HOL/NumberTheory/README Sat Feb 03 17:43:34 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-IntPrimes dvd relation, GCD, Euclid's extended algorithm, primes,
- congruences (all on the Integers)
- Comparable to 'Primes' theory but dvd is included here
- as it is not present in 'IntDiv'. Also includes extended
- GCD and congruences not present in 'Primes'.
-
-Chinese The Chinese Remainder Theorem for an arbitrary finite
- number of equations. (The one-equation case is included
- in 'IntPrimes') Uses functions for indexing.
-
-IntFact Factorial on integers and recursively defined set
- including all Integers from 2 up to a. Plus definition
- of product of finite set.
-
-BijectionRel Inductive definitions of bijections between two different
- sets and between the same set. Theorem for relating
- the two definitions
-
-EulerFermat Fermat's Little Theorem extended to Euler's Totient function.
- More abstract approach than Boyer-Moore (which seems necessary
- to achieve the extended version)
-
-WilsonRuss Wilson's Theorem following quite closely Russinoff's approach
- using Boyer-Moore (using finite sets instead of lists, though)
-
-WilsonBij Wilson's Theorem using a more "abstract" approach based on
- bijections between sets. Does not use Fermat's Little Theorem
- (unlike Russinoff)
-
-
\ No newline at end of file