no open;
authorwenzelm
Wed, 21 Oct 1998 16:06:09 +0200
changeset 5711 5a1cd4b4b20e
parent 5710 30f4d3713cbe
child 5712 18f1c2501343
no open;
src/HOL/AxClasses/Lattice/CLattice.ML
src/HOL/AxClasses/Lattice/LatInsts.ML
src/HOL/AxClasses/Lattice/LatMorph.ML
src/HOL/AxClasses/Lattice/LatPreInsts.ML
src/HOL/AxClasses/Lattice/Lattice.ML
src/HOL/AxClasses/Lattice/OrdDefs.ML
src/HOL/AxClasses/Lattice/Order.ML
src/HOL/AxClasses/Tutorial/Group.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" **)
 
--- 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";
--- 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 **)
--- 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 **)
--- 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 "||" **)
--- 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 **)
--- 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 **)
--- 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);