# HG changeset patch
# User wenzelm
# Date 908978769 -7200
# Node ID 5a1cd4b4b20e8ccb22e624d39ccd5db813941e1c
# Parent  30f4d3713cbeff2e3b53e571b56db22bb0ec21f1
no open;

diff -r 30f4d3713cbe -r 5a1cd4b4b20e src/HOL/AxClasses/Lattice/CLattice.ML
--- a/src/HOL/AxClasses/Lattice/CLattice.ML	Wed Oct 21 16:04:57 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Wed Oct 21 16:06:09 1998 +0200
@@ -1,6 +1,3 @@
-
-open CLattice;
-
 
 (** basic properties of "Inf" and "Sup" **)
 
diff -r 30f4d3713cbe -r 5a1cd4b4b20e src/HOL/AxClasses/Lattice/LatInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatInsts.ML	Wed Oct 21 16:04:57 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Wed Oct 21 16:06:09 1998 +0200
@@ -1,5 +1,3 @@
-
-open LatInsts;
 
 
 Goal "Inf {x, y} = x && y";
diff -r 30f4d3713cbe -r 5a1cd4b4b20e src/HOL/AxClasses/Lattice/LatMorph.ML
--- a/src/HOL/AxClasses/Lattice/LatMorph.ML	Wed Oct 21 16:04:57 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Wed Oct 21 16:06:09 1998 +0200
@@ -1,5 +1,3 @@
-
-open LatMorph;
 
 
 (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
diff -r 30f4d3713cbe -r 5a1cd4b4b20e src/HOL/AxClasses/Lattice/LatPreInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Wed Oct 21 16:04:57 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Wed Oct 21 16:06:09 1998 +0200
@@ -1,5 +1,3 @@
-
-open LatPreInsts;
 
 
 (** complete lattices **)
diff -r 30f4d3713cbe -r 5a1cd4b4b20e src/HOL/AxClasses/Lattice/Lattice.ML
--- a/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Oct 21 16:04:57 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Oct 21 16:06:09 1998 +0200
@@ -1,5 +1,3 @@
-
-open Lattice;
 
 
 (** basic properties of "&&" and "||" **)
diff -r 30f4d3713cbe -r 5a1cd4b4b20e src/HOL/AxClasses/Lattice/OrdDefs.ML
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Oct 21 16:04:57 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Oct 21 16:06:09 1998 +0200
@@ -1,5 +1,3 @@
-
-open OrdDefs;
 
 
 (** lifting of quasi / partial orders **)
diff -r 30f4d3713cbe -r 5a1cd4b4b20e src/HOL/AxClasses/Lattice/Order.ML
--- a/src/HOL/AxClasses/Lattice/Order.ML	Wed Oct 21 16:04:57 1998 +0200
+++ b/src/HOL/AxClasses/Lattice/Order.ML	Wed Oct 21 16:06:09 1998 +0200
@@ -1,5 +1,3 @@
-
-open Order;
 
 
 (** basic properties of limits **)
diff -r 30f4d3713cbe -r 5a1cd4b4b20e src/HOL/AxClasses/Tutorial/Group.ML
--- a/src/HOL/AxClasses/Tutorial/Group.ML	Wed Oct 21 16:04:57 1998 +0200
+++ b/src/HOL/AxClasses/Tutorial/Group.ML	Wed Oct 21 16:06:09 1998 +0200
@@ -5,8 +5,6 @@
 Some basic theorems of group theory.
 *)
 
-open Group;
-
 fun sub r = standard (r RS subst);
 fun ssub r = standard (r RS ssubst);