src/HOL/NumberTheory/IntPrimes.thy

--- a/src/HOL/NumberTheory/IntPrimes.thy	Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu Dec 08 12:50:04 2005 +0100
@@ -2,11 +2,6 @@
     ID:         $Id$
     Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
-
-Changes by Jeremy Avigad, 2003/02/21:
-   Repaired definition of zprime_def, added "0 <= m &"
-   Added lemma zgcd_geq_zero
-   Repaired proof of zprime_imp_zrelprime
 *)
 
 header {* Divisibility and prime numbers (on integers) *}