author | wenzelm |
Tue, 29 Apr 1997 17:13:41 +0200 | |
changeset 3065 | c57861f709d2 |
parent 3064 | f04f93e5c0a9 |
child 3066 | 3c548f92e032 |
src/ZF/ZF.thy | file | annotate | diff | comparison | revisions |
--- 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