added \<langle>, \<rangle> symbols syntax;
authorwenzelm
Tue, 29 Apr 1997 17:13:41 +0200
changeset 3065 c57861f709d2
parent 3064 f04f93e5c0a9
child 3066 3c548f92e032
added \<langle>, \<rangle> symbols syntax;
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