# HG changeset patch
# User wenzelm
# Date 862326821 -7200
# Node ID c57861f709d29532a38d478279caec349abbb91e
# Parent  f04f93e5c0a9245d10664202f640cee9d710516c
added \<langle>, \<rangle> symbols syntax;

diff -r f04f93e5c0a9 -r c57861f709d2 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue Apr 29 16:39:13 1997 +0200
+++ b/src/ZF/ZF.thy	Tue Apr 29 17:13:41 1997 +0200
@@ -149,6 +149,8 @@
   "@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)
+  "@Tuple"    :: [i, is] => i              ("\\<langle>(_,/ _)\\<rangle>")
+  "@pttrn"    :: pttrns => pttrn           ("\\<langle>_\\<rangle>")
 
 
 defs