--- 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)";
--- 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) + \
--- 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";
--- 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 *)
(* ############################################################ *)
--- 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 **)
(************************************************)