Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/NumberTheory/README
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)
isabelle