# HG changeset patch
# User paulson
# Date 910605529 -3600
# Node ID bacf85370ce0843aa213ed27eda1c537fbc775d9
# Parent  f174f3be058f9b16e2e57b3e016f9beb594bd2b7
removed obsolete comment and "open" declaration

diff -r f174f3be058f -r bacf85370ce0 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 "=";
diff -r f174f3be058f -r bacf85370ce0 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Nov 06 15:48:37 1998 +0100
+++ b/src/HOL/Univ.ML	Mon Nov 09 10:58:49 1998 +0100
@@ -2,12 +2,8 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
-
-For univ.thy
 *)
 
-open Univ;
-
 (** apfst -- can be used in similar type definitions **)
 
 Goalw [apfst_def] "apfst f (a,b) = (f(a),b)";
diff -r f174f3be058f -r bacf85370ce0 src/ZF/AC.ML
--- a/src/ZF/AC.ML	Fri Nov 06 15:48:37 1998 +0100
+++ b/src/ZF/AC.ML	Mon Nov 09 10:58:49 1998 +0100
@@ -3,11 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-For AC.thy.  The Axiom of Choice
+The Axiom of Choice
 *)
 
-open AC;
-
 (*The same as AC, but no premise a:A*)
 val [nonempty] = goal AC.thy
      "[| !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)";
diff -r f174f3be058f -r bacf85370ce0 src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Fri Nov 06 15:48:37 1998 +0100
+++ b/src/ZF/Epsilon.ML	Mon Nov 09 10:58:49 1998 +0100
@@ -3,11 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For epsilon.thy.  Epsilon induction and recursion
+Epsilon induction and recursion
 *)
 
-open Epsilon;
-
 (*** Basic closure properties ***)
 
 Goalw [eclose_def] "A <= eclose(A)";
diff -r f174f3be058f -r bacf85370ce0 src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Fri Nov 06 15:48:37 1998 +0100
+++ b/src/ZF/QUniv.ML	Mon Nov 09 10:58:49 1998 +0100
@@ -3,11 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For quniv.thy.  A small universe for lazy recursive types
+A small universe for lazy recursive types
 *)
 
-open QUniv;
-
 (** Properties involving Transset and Sum **)
 
 val [prem1,prem2] = goalw QUniv.thy [sum_def]