added symbols syntax;
authorwenzelm
Thu Jan 23 12:42:07 1997 +0100 (1997-01-23)
changeset 2540ba8311047f18
parent 2539 ddd22ceee8cc
child 2541 70aa00ed3025
added symbols syntax;
src/ZF/OrdQuant.thy
src/ZF/Ordinal.thy
src/ZF/ZF.thy
     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 *)
     2.1 --- a/src/ZF/Ordinal.thy	Thu Jan 23 10:40:21 1997 +0100
     2.2 +++ b/src/ZF/Ordinal.thy	Thu Jan 23 12:42:07 1997 +0100
     2.3 @@ -19,6 +19,9 @@
     2.4  translations
     2.5    "x le y"      == "x < succ(y)"
     2.6  
     2.7 +syntax (symbols)
     2.8 +  "op le"       :: [i,i] => o  (infixl "\\<le>" 50) (*less than or equals*)
     2.9 +
    2.10  defs
    2.11    Memrel_def    "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
    2.12    Transset_def  "Transset(i) == ALL x:i. x<=i"
     3.1 --- a/src/ZF/ZF.thy	Thu Jan 23 10:40:21 1997 +0100
     3.2 +++ b/src/ZF/ZF.thy	Thu Jan 23 12:42:07 1997 +0100
     3.3 @@ -132,6 +132,25 @@
     3.4    "%<x,y>.b"    == "split(%x y.b)"
     3.5  
     3.6  
     3.7 +syntax (symbols)
     3.8 +  "op *"      :: [i, i] => i               (infixr "\\<times>" 80)
     3.9 +  "op Int"    :: [i, i] => i    	   (infixl "\\<inter>" 70)
    3.10 +  "op Un"     :: [i, i] => i    	   (infixl "\\<union>" 65)
    3.11 +  "op ->"     :: [i, i] => i               (infixr "\\<rightarrow>" 60)
    3.12 +  "op <="     :: [i, i] => o    	   (infixl "\\<subseteq>" 50)
    3.13 +  "op :"      :: [i, i] => o    	   (infixl "\\<in>" 50)
    3.14 +  "op ~:"     :: [i, i] => o               (infixl "\\<notin>" 50)
    3.15 +  "@Collect"  :: [pttrn, i, o] => i        ("(1{_\\<in> _ ./ _})")
    3.16 +  "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _\\<in> _, _})")
    3.17 +  "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _\\<in> _})" [51,0,51])
    3.18 +  "@INTER"    :: [pttrn, i, i] => i        ("(3\\<Inter> _\\<in>_./ _)" 10)
    3.19 +  "@UNION"    :: [pttrn, i, i] => i        ("(3\\<Union> _\\<in>_./ _)" 10)
    3.20 +  "@PROD"     :: [pttrn, i, i] => i        ("(3\\<Pi> _\\<in>_./ _)" 10)
    3.21 +  "@SUM"      :: [pttrn, i, i] => i        ("(3\\<Sigma> _\\<in>_./ _)" 10)
    3.22 +  "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall> _\\<in>_./ _)" 10)
    3.23 +  "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists> _\\<in>_./ _)" 10)
    3.24 +
    3.25 +
    3.26  defs
    3.27  
    3.28    (* Bounded Quantifiers *)