--- a/src/ZF/OrdQuant.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/OrdQuant.ML Wed Jan 13 11:57:09 1999 +0100
@@ -5,8 +5,6 @@
Quantifiers and union operator for ordinals.
*)
-open OrdQuant;
-
(*** universal quantifier for ordinals ***)
qed_goalw "oallI" thy [oall_def]