isabelle: src/HOL/NumberTheory/ROOT.ML@8408a06590a6 (annotated)

13871 26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	1	(* Title: HOL/NumberTheory/ROOT.ML
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	2	ID: $Id$
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	3	Author: Lawrence C Paulson
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	4	Copyright 2003 University of Cambridge
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	5
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	6	This directory contains formalized proofs of Wilson's Theorem (by Thomas M
13887 54a0c675c423 tidied paulson parents: 13871 diff changeset	7	Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and
54a0c675c423 tidied paulson parents: 13871 diff changeset	8	Kramer).
54a0c675c423 tidied paulson parents: 13871 diff changeset	9
54a0c675c423 tidied paulson parents: 13871 diff changeset	10	The quadratic reciprocity formalization follows Eisenstein's proof, which is
54a0c675c423 tidied paulson parents: 13871 diff changeset	11	the one most commonly found in introductory textbooks, and also uses a trick
54a0c675c423 tidied paulson parents: 13871 diff changeset	12	used David Russinoff with the Boyer-Moore theorem prover. See his "A
54a0c675c423 tidied paulson parents: 13871 diff changeset	13	mechanical proof of quadratic reciprocity," Journal of Automated Reasoning
54a0c675c423 tidied paulson parents: 13871 diff changeset	14	8:3-21, 1992.*)
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	15
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	16	no_document use_thy "Permutation";
11368 9c1995c73383 tuned Primes theory; wenzelm parents: 11049 diff changeset	17	no_document use_thy "Primes";
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	18
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	19	use_thy "Fib";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	20	use_thy "Factorization";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	21	use_thy "Chinese";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	22	use_thy "WilsonRuss";
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 9944 diff changeset	23	use_thy "WilsonBij";
13871 26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer paulson parents: 11368 diff changeset	24	use_thy "Quadratic_Reciprocity";

author	paulson
	Tue, 29 Mar 2005 12:30:48 +0200
changeset 15635	8408a06590a6
parent 14271	8ed6989228bb
child 19671	e293e16d1442
permissions	-rw-r--r--