src/ZF/OrdQuant.thy
changeset 3923 c257b82a1200
parent 2540 ba8311047f18
child 3940 1d5bee4d047f
     1.1 --- a/src/ZF/OrdQuant.thy	Fri Oct 17 17:39:04 1997 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Fri Oct 17 17:40:02 1997 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  OrdQuant = Ordinal +
     1.6  
     1.7 +global
     1.8 +
     1.9  consts
    1.10    
    1.11    (* Ordinal Quantifiers *)
    1.12 @@ -30,6 +32,7 @@
    1.13    "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
    1.14    "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    1.15  
    1.16 +path OrdQuant
    1.17  
    1.18  defs
    1.19