# HG changeset patch
# User paulson
# Date 1049106566 -7200
# Node ID 54a0c675c4231c464a24a1be7ccbb4d347ac2239
# Parent  0b243f6e257e8a795a311c2c12eb27632c8a33f1
tidied

diff -r 0b243f6e257e -r 54a0c675c423 src/HOL/NumberTheory/ROOT.ML
--- 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";