src/HOL/HOL.ML

--- a/src/HOL/HOL.ML	Fri Nov 06 15:48:37 1998 +0100
+++ b/src/HOL/HOL.ML	Mon Nov 09 10:58:49 1998 +0100
@@ -3,12 +3,9 @@
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
 
-For HOL.thy
 Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 
 *)
 
-open HOL;
-
 
 (** Equality **)
 section "=";