paulson@13871: (* Title: HOL/NumberTheory/ROOT.ML
paulson@13871: ID: $Id$
paulson@13871: Author: Lawrence C Paulson
paulson@13871: Copyright 2003 University of Cambridge
paulson@13871:
paulson@13871: This directory contains formalized proofs of Wilson's Theorem (by Thomas M
paulson@13887: Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and
paulson@13887: Kramer).
paulson@13887:
paulson@13887: The quadratic reciprocity formalization follows Eisenstein's proof, which is
paulson@13887: the one most commonly found in introductory textbooks, and also uses a trick
paulson@13887: used David Russinoff with the Boyer-Moore theorem prover. See his "A
paulson@13887: mechanical proof of quadratic reciprocity," Journal of Automated Reasoning
paulson@13887: 8:3-21, 1992.*)
paulson@9508:
wenzelm@11049: no_document use_thy "Permutation";
wenzelm@11368: no_document use_thy "Primes";
paulson@9508:
wenzelm@11049: use_thy "Fib";
wenzelm@11049: use_thy "Factorization";
wenzelm@11049: use_thy "Chinese";
wenzelm@11049: use_thy "EulerFermat";
wenzelm@11049: use_thy "WilsonRuss";
wenzelm@11049: use_thy "WilsonBij";
paulson@13871: use_thy "Quadratic_Reciprocity";