# HG changeset patch
# User paulson
# Date 965636855 -7200
# Node ID c1d9500e292780c4e97f42f2bf6f36d57262a859
# Parent  f9202e219a295c0b01a510fcf3f532d36fb102b0
tidied

diff -r f9202e219a29 -r c1d9500e2927 src/HOL/NumberTheory/README
--- 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)