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";