changeset 9545 c1d9500e2927 parent 9508 4d01dbf6ded7
```--- a/src/HOL/NumberTheory/README	Mon Aug 07 10:27:11 2000 +0200
+++ b/src/HOL/NumberTheory/README	Mon Aug 07 10:27:35 2000 +0200
@@ -1,29 +1,22 @@
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
+                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?
+                number of equations.  (The one-equation case is included
+                in 'IntPrimes')  Uses functions for indexing.

-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?
+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
+                sets and between the same set.  Theorem for relating
the two definitions

-EulerFermat     Fermat's Little Theorem extended to Euler's Totient function.
+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)
```