# HG changeset patch
# User paulson
# Date 901875801 -7200
# Node ID e5a6ace920a0fff2e88200771f0428c1536c8eb0
# Parent  89934cd022a93b215ede9408410c840014e23eb8
Removal of obsolete "open" commands from heads of .ML files

diff -r 89934cd022a9 -r e5a6ace920a0 src/HOL/ex/BT.ML
--- a/src/HOL/ex/BT.ML	Fri Jul 31 10:54:39 1998 +0200
+++ b/src/HOL/ex/BT.ML	Fri Jul 31 11:03:21 1998 +0200
@@ -6,8 +6,6 @@
 Datatype definition of binary trees
 *)
 
-open BT;
-
 (** BT simplification **)
 
 Goal "n_leaves(reflect(t)) = n_leaves(t)";
diff -r 89934cd022a9 -r e5a6ace920a0 src/HOL/ex/IntRing.ML
--- a/src/HOL/ex/IntRing.ML	Fri Jul 31 10:54:39 1998 +0200
+++ b/src/HOL/ex/IntRing.ML	Fri Jul 31 11:03:21 1998 +0200
@@ -6,8 +6,6 @@
 The instantiation of Lagrange's lemma for int.
 *)
 
-open IntRing;
-
 Goal "!!i1::int. \
 \  (sq i1 + sq i2 + sq i3 + sq i4) * (sq j1 + sq j2 + sq j3 + sq j4) = \
 \  sq(i1*j1 - i2*j2 - i3*j3 - i4*j4)  + \
diff -r 89934cd022a9 -r e5a6ace920a0 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";
diff -r 89934cd022a9 -r e5a6ace920a0 src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Fri Jul 31 10:54:39 1998 +0200
+++ b/src/HOL/ex/MT.ML	Fri Jul 31 11:03:21 1998 +0200
@@ -15,8 +15,6 @@
 NEEDS TO USE INDUCTIVE DEFS PACKAGE
 *)
 
-open MT;
-
 (* ############################################################ *)
 (* Inference systems                                            *)
 (* ############################################################ *)
diff -r 89934cd022a9 -r e5a6ace920a0 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Fri Jul 31 10:54:39 1998 +0200
+++ b/src/HOL/ex/Primes.ML	Fri Jul 31 11:03:21 1998 +0200
@@ -10,8 +10,6 @@
 
 eta_contract:=false;
 
-open Primes;
-
 (************************************************)
 (** Greatest Common Divisor                    **)
 (************************************************)