--- 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