src/HOL/ex/IntRingDefs.ML

--- a/src/HOL/ex/IntRingDefs.ML	Fri Jul 31 10:54:39 1998 +0200
+++ b/src/HOL/ex/IntRingDefs.ML	Fri Jul 31 11:03:21 1998 +0200
@@ -2,11 +2,8 @@
     ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel
     Copyright   1996 TU Muenchen
-
 *)
 
-open IntRingDefs;
-
 Goalw [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
 by (Simp_tac 1);
 qed "left_inv_int";