--- 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)