summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/NumberTheory/ROOT.ML

changeset 13887 | 54a0c675c423 |

parent 13871 | 26e5f5e624f6 |

child 14271 | 8ed6989228bb |

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