summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/NumberTheory/ROOT.ML

changeset 13887 | 54a0c675c423 |

parent 13871 | 26e5f5e624f6 |

child 14271 | 8ed6989228bb |

1.1 --- a/src/HOL/NumberTheory/ROOT.ML Sat Mar 29 12:28:53 2003 +0100 1.2 +++ b/src/HOL/NumberTheory/ROOT.ML Mon Mar 31 12:29:26 2003 +0200 1.3 @@ -4,13 +4,14 @@ 1.4 Copyright 2003 University of Cambridge 1.5 1.6 This directory contains formalized proofs of Wilson's Theorem (by Thomas M 1.7 -Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and 1.8 -Kramer). The latter formalization follows Eisenstein's proof, which is the 1.9 -one most commonly found in introductory textbooks, and also uses a 1.10 -trick used David Russinoff with the Boyer-Moore theorem prover. 1.11 -See his "A mechanical proof of quadratic reciprocity," Journal of Automated 1.12 -Reasoning 8:3-21, 1992. 1.13 -*) 1.14 +Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and 1.15 +Kramer). 1.16 + 1.17 +The quadratic reciprocity formalization follows Eisenstein's proof, which is 1.18 +the one most commonly found in introductory textbooks, and also uses a trick 1.19 +used David Russinoff with the Boyer-Moore theorem prover. See his "A 1.20 +mechanical proof of quadratic reciprocity," Journal of Automated Reasoning 1.21 +8:3-21, 1992.*) 1.22 1.23 no_document use_thy "Permutation"; 1.24 no_document use_thy "Primes";