src/HOL/NumberTheory/ROOT.ML
changeset 13887 54a0c675c423
parent 13871 26e5f5e624f6
child 14271 8ed6989228bb
equal deleted inserted replaced
13886:0b243f6e257e 13887:54a0c675c423
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     3     Author:     Lawrence C Paulson
     4     Copyright   2003  University of Cambridge
     4     Copyright   2003  University of Cambridge
     5 
     5 
     6 This directory contains formalized proofs of Wilson's Theorem (by Thomas M
     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
     7 Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and
     8 Kramer).  The latter formalization follows Eisenstein's proof, which is the
     8 Kramer).  
     9 one most commonly found in introductory textbooks, and also uses a
     9 
    10 trick used David Russinoff with the Boyer-Moore theorem prover.
    10 The quadratic reciprocity formalization follows Eisenstein's proof, which is
    11 See his "A mechanical proof of quadratic reciprocity," Journal of Automated
    11 the one most commonly found in introductory textbooks, and also uses a trick
    12 Reasoning 8:3-21, 1992.
    12 used David Russinoff with the Boyer-Moore theorem prover.  See his "A
    13 *)
    13 mechanical proof of quadratic reciprocity," Journal of Automated Reasoning
       
    14 8:3-21, 1992.*)
    14 
    15 
    15 no_document use_thy "Permutation";
    16 no_document use_thy "Permutation";
    16 no_document use_thy "Primes";
    17 no_document use_thy "Primes";
    17 
    18 
    18 use_thy "Fib";
    19 use_thy "Fib";