summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Mon, 07 Aug 2000 10:27:35 +0200 | |

changeset 9545 | c1d9500e2927 |

parent 9544 | f9202e219a29 |

child 9546 | be095014e72f |

tidied

--- 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)