src/HOL/NumberTheory/ROOT.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14271 8ed6989228bb
child 19671 e293e16d1442
permissions -rw-r--r--
import -> imports
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@13887
     7
Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and
paulson@13887
     8
Kramer).  
paulson@13887
     9
paulson@13887
    10
The quadratic reciprocity formalization follows Eisenstein's proof, which is
paulson@13887
    11
the one most commonly found in introductory textbooks, and also uses a trick
paulson@13887
    12
used David Russinoff with the Boyer-Moore theorem prover.  See his "A
paulson@13887
    13
mechanical proof of quadratic reciprocity," Journal of Automated Reasoning
paulson@13887
    14
8:3-21, 1992.*)
paulson@9508
    15
wenzelm@11049
    16
no_document use_thy "Permutation";
wenzelm@11368
    17
no_document use_thy "Primes";
paulson@9508
    18
wenzelm@11049
    19
use_thy "Fib";
wenzelm@11049
    20
use_thy "Factorization";
wenzelm@11049
    21
use_thy "Chinese";
wenzelm@11049
    22
use_thy "WilsonRuss";
wenzelm@11049
    23
use_thy "WilsonBij";
paulson@13871
    24
use_thy "Quadratic_Reciprocity";