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
     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's law of quadratic reciprocity (by Avigad, Gray and
     8 Kramer).  
     9 
    10 The quadratic reciprocity formalization follows Eisenstein's proof, which is
    11 the one most commonly found in introductory textbooks, and also uses a trick
    12 used David Russinoff with the Boyer-Moore theorem prover.  See his "A
    13 mechanical proof of quadratic reciprocity," Journal of Automated Reasoning
    14 8:3-21, 1992.*)
    15 
    16 no_document use_thy "Permutation";
    17 no_document use_thy "Primes";
    18 
    19 use_thy "Fib";
    20 use_thy "Factorization";
    21 use_thy "Chinese";
    22 use_thy "WilsonRuss";
    23 use_thy "WilsonBij";
    24 use_thy "Quadratic_Reciprocity";