summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/NumberTheory/ROOT.ML

changeset 13871 | 26e5f5e624f6 |

parent 11368 | 9c1995c73383 |

child 13887 | 54a0c675c423 |

1.1 --- a/src/HOL/NumberTheory/ROOT.ML Tue Mar 18 18:07:06 2003 +0100 1.2 +++ b/src/HOL/NumberTheory/ROOT.ML Thu Mar 20 15:58:25 2003 +0100 1.3 @@ -1,3 +1,16 @@ 1.4 +(* Title: HOL/NumberTheory/ROOT.ML 1.5 + ID: $Id$ 1.6 + Author: Lawrence C Paulson 1.7 + Copyright 2003 University of Cambridge 1.8 + 1.9 +This directory contains formalized proofs of Wilson's Theorem (by Thomas M 1.10 +Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and 1.11 +Kramer). The latter formalization follows Eisenstein's proof, which is the 1.12 +one most commonly found in introductory textbooks, and also uses a 1.13 +trick used David Russinoff with the Boyer-Moore theorem prover. 1.14 +See his "A mechanical proof of quadratic reciprocity," Journal of Automated 1.15 +Reasoning 8:3-21, 1992. 1.16 +*) 1.17 1.18 no_document use_thy "Permutation"; 1.19 no_document use_thy "Primes"; 1.20 @@ -8,3 +21,4 @@ 1.21 use_thy "EulerFermat"; 1.22 use_thy "WilsonRuss"; 1.23 use_thy "WilsonBij"; 1.24 +use_thy "Quadratic_Reciprocity";