--- 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 "=";
--- 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)";
--- 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)";
--- 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)";
--- 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]