src/ZF/OrdQuant.thy

--- a/src/ZF/OrdQuant.thy	Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/OrdQuant.thy	Fri Oct 17 17:40:02 1997 +0200
@@ -7,6 +7,8 @@
 
 OrdQuant = Ordinal +
 
+global
+
 consts
   
   (* Ordinal Quantifiers *)
@@ -30,6 +32,7 @@
   "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
   "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
 
+path OrdQuant
 
 defs