# HG changeset patch
# User wenzelm
# Date 854019727 -3600
# Node ID ba8311047f18295bf2fc8de7d0c1bc8a0ab6478f
# Parent  ddd22ceee8cc17b7d3e3bb7b266387022aff6298
added symbols syntax;

diff -r ddd22ceee8cc -r ba8311047f18 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Thu Jan 23 10:40:21 1997 +0100
+++ b/src/ZF/OrdQuant.thy	Thu Jan 23 12:42:07 1997 +0100
@@ -16,17 +16,21 @@
   OUnion      :: [i, i => i] => i
   
 syntax
-  
   "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
   "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
   "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
 
 translations
-  
   "ALL x<a. P"  == "oall(a, %x. P)"
   "EX x<a. P"   == "oex(a, %x. P)"
   "UN x<a. B"   == "OUnion(a, %x. B)"
 
+syntax (symbols)
+  "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
+  "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
+  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
+
+
 defs
   
   (* Ordinal Quantifiers *)
diff -r ddd22ceee8cc -r ba8311047f18 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Thu Jan 23 10:40:21 1997 +0100
+++ b/src/ZF/Ordinal.thy	Thu Jan 23 12:42:07 1997 +0100
@@ -19,6 +19,9 @@
 translations
   "x le y"      == "x < succ(y)"
 
+syntax (symbols)
+  "op le"       :: [i,i] => o  (infixl "\\<le>" 50) (*less than or equals*)
+
 defs
   Memrel_def    "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
   Transset_def  "Transset(i) == ALL x:i. x<=i"
diff -r ddd22ceee8cc -r ba8311047f18 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Jan 23 10:40:21 1997 +0100
+++ b/src/ZF/ZF.thy	Thu Jan 23 12:42:07 1997 +0100
@@ -132,6 +132,25 @@
   "%<x,y>.b"    == "split(%x y.b)"
 
 
+syntax (symbols)
+  "op *"      :: [i, i] => i               (infixr "\\<times>" 80)
+  "op Int"    :: [i, i] => i    	   (infixl "\\<inter>" 70)
+  "op Un"     :: [i, i] => i    	   (infixl "\\<union>" 65)
+  "op ->"     :: [i, i] => i               (infixr "\\<rightarrow>" 60)
+  "op <="     :: [i, i] => o    	   (infixl "\\<subseteq>" 50)
+  "op :"      :: [i, i] => o    	   (infixl "\\<in>" 50)
+  "op ~:"     :: [i, i] => o               (infixl "\\<notin>" 50)
+  "@Collect"  :: [pttrn, i, o] => i        ("(1{_\\<in> _ ./ _})")
+  "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _\\<in> _, _})")
+  "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _\\<in> _})" [51,0,51])
+  "@INTER"    :: [pttrn, i, i] => i        ("(3\\<Inter> _\\<in>_./ _)" 10)
+  "@UNION"    :: [pttrn, i, i] => i        ("(3\\<Union> _\\<in>_./ _)" 10)
+  "@PROD"     :: [pttrn, i, i] => i        ("(3\\<Pi> _\\<in>_./ _)" 10)
+  "@SUM"      :: [pttrn, i, i] => i        ("(3\\<Sigma> _\\<in>_./ _)" 10)
+  "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall> _\\<in>_./ _)" 10)
+  "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists> _\\<in>_./ _)" 10)
+
+
 defs
 
   (* Bounded Quantifiers *)