# HG changeset patch
# User wenzelm
# Date 968969992 -7200
# Node ID 1971c8dd09710373f9fff7dfca9b46f7e5717319
# Parent  7966a29022666b9b43cf7c5561a5e9bf0a45f369
tuned spacing of symbols syntax;
enabled langle and rangle in xsymbols syntax;

diff -r 7966a2902266 -r 1971c8dd0971 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Sep 15 00:18:36 2000 +0200
+++ b/src/ZF/ZF.thy	Fri Sep 15 00:19:52 2000 +0200
@@ -153,17 +153,17 @@
   "@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)
-  "@lam"      :: [pttrn, i, i] => i        ("(3\\<lambda> _:_./ _)" 10)
-  "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall> _\\<in>_./ _)" 10)
-  "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists> _\\<in>_./ _)" 10)
-(*
+  "@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)
+  "@lam"      :: [pttrn, i, i] => i        ("(3\\<lambda>_:_./ _)" 10)
+  "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall>_\\<in>_./ _)" 10)
+  "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists>_\\<in>_./ _)" 10)
+
+syntax (xsymbols)
   "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
   "@pattern"  :: patterns => pttrn         ("\\<langle>_\\<rangle>")
-*)
 
 syntax (HTML output)
   "op *"      :: [i, i] => i               (infixr "\\<times>" 80)