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
paulson@13871
     1
(*  Title:      HOL/NumberTheory/ROOT.ML
paulson@13871
     2
    ID:         $Id$
paulson@13871
     3
    Author:     Lawrence C Paulson
paulson@13871
     4
    Copyright   2003  University of Cambridge
paulson@13871
     5
paulson@13871
     6
This directory contains formalized proofs of Wilson's Theorem (by Thomas M
paulson@13871
     7
Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and
paulson@13871
     8
Kramer).  The latter formalization follows Eisenstein's proof, which is the
paulson@13871
     9
one most commonly found in introductory textbooks, and also uses a
paulson@13871
    10
trick used David Russinoff with the Boyer-Moore theorem prover.
paulson@13871
    11
See his "A mechanical proof of quadratic reciprocity," Journal of Automated
paulson@13871
    12
Reasoning 8:3-21, 1992.
paulson@13871
    13
*)
paulson@9508
    14
wenzelm@11049
    15
no_document use_thy "Permutation";
wenzelm@11368
    16
no_document use_thy "Primes";
paulson@9508
    17
wenzelm@11049
    18
use_thy "Fib";
wenzelm@11049
    19
use_thy "Factorization";
wenzelm@11049
    20
use_thy "Chinese";
wenzelm@11049
    21
use_thy "EulerFermat";
wenzelm@11049
    22
use_thy "WilsonRuss";
wenzelm@11049
    23
use_thy "WilsonBij";
paulson@13871
    24
use_thy "Quadratic_Reciprocity";