# HG changeset patch
# User wenzelm
# Date 1147821823 -7200
# Node ID e293e16d14425159e8fe6d9c9c1e12535a481e23
# Parent  2e4a143c73c5de431e17d97c0c6bbacb0e8e86a9
removed outdated/redundant comments;

diff -r 2e4a143c73c5 -r e293e16d1442 src/HOL/NumberTheory/ROOT.ML
--- a/src/HOL/NumberTheory/ROOT.ML	Wed May 17 01:23:41 2006 +0200
+++ b/src/HOL/NumberTheory/ROOT.ML	Wed May 17 01:23:43 2006 +0200
@@ -1,17 +1,4 @@
-(*  Title:      HOL/NumberTheory/ROOT.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson
-    Copyright   2003  University of Cambridge
-
-This directory contains formalized proofs of Wilson's Theorem (by Thomas M
-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.*)
+(* $Id$ *)
 
 no_document use_thy "Permutation";
 no_document use_thy "Primes";