src/HOL/NumberTheory/ROOT.ML
changeset 13871 26e5f5e624f6
parent 11368 9c1995c73383
child 13887 54a0c675c423
     1.1 --- a/src/HOL/NumberTheory/ROOT.ML	Tue Mar 18 18:07:06 2003 +0100
     1.2 +++ b/src/HOL/NumberTheory/ROOT.ML	Thu Mar 20 15:58:25 2003 +0100
     1.3 @@ -1,3 +1,16 @@
     1.4 +(*  Title:      HOL/NumberTheory/ROOT.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson
     1.7 +    Copyright   2003  University of Cambridge
     1.8 +
     1.9 +This directory contains formalized proofs of Wilson's Theorem (by Thomas M
    1.10 +Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and
    1.11 +Kramer).  The latter formalization follows Eisenstein's proof, which is the
    1.12 +one most commonly found in introductory textbooks, and also uses a
    1.13 +trick used David Russinoff with the Boyer-Moore theorem prover.
    1.14 +See his "A mechanical proof of quadratic reciprocity," Journal of Automated
    1.15 +Reasoning 8:3-21, 1992.
    1.16 +*)
    1.17  
    1.18  no_document use_thy "Permutation";
    1.19  no_document use_thy "Primes";
    1.20 @@ -8,3 +21,4 @@
    1.21  use_thy "EulerFermat";
    1.22  use_thy "WilsonRuss";
    1.23  use_thy "WilsonBij";
    1.24 +use_thy "Quadratic_Reciprocity";