author wenzelm Wed, 17 May 2006 01:23:44 +0200 changeset 19672 9be07d531694 parent 19671 e293e16d1442 child 19673 853f5a3cc06e
tuned;
--- a/src/HOL/NumberTheory/document/root.tex	Wed May 17 01:23:43 2006 +0200
+++ b/src/HOL/NumberTheory/document/root.tex	Wed May 17 01:23:44 2006 +0200
@@ -17,7 +17,7 @@
\maketitle

\begin{abstract}
-This directory contains formalized proofs of many results of number theory.
+This is a collection of formalized proofs of many results of number theory.
The proofs of the Chinese Remainder Theorem and Wilson's Theorem are due to
Rasmussen.  The proof of Gauss's law of quadratic reciprocity is due to
Avigad, Gray and Kramer.  Proofs can be found in most introductory number