src/HOL/NumberTheory/ROOT.ML
author paulson
Thu Mar 20 15:58:25 2003 +0100 (2003-03-20)
changeset 13871 26e5f5e624f6
parent 11368 9c1995c73383
child 13887 54a0c675c423
permissions -rw-r--r--
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
     1 (*  Title:      HOL/NumberTheory/ROOT.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   2003  University of Cambridge
     5 
     6 This directory contains formalized proofs of Wilson's Theorem (by Thomas M
     7 Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and
     8 Kramer).  The latter formalization follows Eisenstein's proof, which is the
     9 one most commonly found in introductory textbooks, and also uses a
    10 trick used David Russinoff with the Boyer-Moore theorem prover.
    11 See his "A mechanical proof of quadratic reciprocity," Journal of Automated
    12 Reasoning 8:3-21, 1992.
    13 *)
    14 
    15 no_document use_thy "Permutation";
    16 no_document use_thy "Primes";
    17 
    18 use_thy "Fib";
    19 use_thy "Factorization";
    20 use_thy "Chinese";
    21 use_thy "EulerFermat";
    22 use_thy "WilsonRuss";
    23 use_thy "WilsonBij";
    24 use_thy "Quadratic_Reciprocity";