src/ZF/OrdQuant.thy
changeset 2540 ba8311047f18
parent 2469 b50b8c0eec01
child 3923 c257b82a1200
     1.1 --- a/src/ZF/OrdQuant.thy	Thu Jan 23 10:40:21 1997 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Thu Jan 23 12:42:07 1997 +0100
     1.3 @@ -16,17 +16,21 @@
     1.4    OUnion      :: [i, i => i] => i
     1.5    
     1.6  syntax
     1.7 -  
     1.8    "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
     1.9    "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
    1.10    "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
    1.11  
    1.12  translations
    1.13 -  
    1.14    "ALL x<a. P"  == "oall(a, %x. P)"
    1.15    "EX x<a. P"   == "oex(a, %x. P)"
    1.16    "UN x<a. B"   == "OUnion(a, %x. B)"
    1.17  
    1.18 +syntax (symbols)
    1.19 +  "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
    1.20 +  "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
    1.21 +  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    1.22 +
    1.23 +
    1.24  defs
    1.25    
    1.26    (* Ordinal Quantifiers *)