--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NumberTheory/README	Thu Aug 03 10:46:01 2000 +0200
@@ -0,0 +1,37 @@
+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'. 
+                Also a few extra theorems concerning 'mod'
+                Maybe it should be split/merged - at least given another
+                name?
+
+Chinese		The Chinese Remainder Theorem for an arbitrary finite
+                number of equations. (The one-equation case is included
+                in 'IntPrimes')
+		Uses functions for indicing. Maybe 'funprod' and 'funsum'
+                should be based on general 'fold' on indices?
+
+IntPowerFact    Power function on Integers (exponent is still Nat),
+                Factorial on integers and recursively defined set
+                including all Integers from 2 up to a. Plus definition 
+		of product of finite set.
+                Should probably be split/merged with other theories?
+
+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