--- a/src/HOL/NumberTheory/ROOT.ML Sat Mar 29 12:28:53 2003 +0100
+++ b/src/HOL/NumberTheory/ROOT.ML Mon Mar 31 12:29:26 2003 +0200
@@ -4,13 +4,14 @@
Copyright 2003 University of Cambridge
This directory contains formalized proofs of Wilson's Theorem (by Thomas M
-Rasmussen) and of Gauss' law of quadratic reciprocity (by Avigad, Gray and
-Kramer). The latter formalization follows Eisenstein's proof, which is the
-one most commonly found in introductory textbooks, and also uses a
-trick used David Russinoff with the Boyer-Moore theorem prover.
-See his "A mechanical proof of quadratic reciprocity," Journal of Automated
-Reasoning 8:3-21, 1992.
-*)
+Rasmussen) and of Gauss's law of quadratic reciprocity (by Avigad, Gray and
+Kramer).
+
+The quadratic reciprocity formalization follows Eisenstein's proof, which is
+the one most commonly found in introductory textbooks, and also uses a trick
+used David Russinoff with the Boyer-Moore theorem prover. See his "A
+mechanical proof of quadratic reciprocity," Journal of Automated Reasoning
+8:3-21, 1992.*)
no_document use_thy "Permutation";
no_document use_thy "Primes";