# HG changeset patch # User wenzelm # Date 1147821824 -7200 # Node ID 9be07d53169495097bc20de1b76aca745b179d14 # Parent e293e16d14425159e8fe6d9c9c1e12535a481e23 tuned; diff -r e293e16d1442 -r 9be07d531694 src/HOL/NumberTheory/document/root.tex --- 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