author | paulson |
Wed, 08 May 2002 10:14:07 +0200 | |
changeset 13119 | 6f7526467e5a |
parent 13118 | 336b0bcbd27c |
child 13120 | d1fea11b2fb6 |
src/ZF/Order.thy | file | annotate | diff | comparison | revisions |
--- a/src/ZF/Order.thy Wed May 08 10:12:57 2002 +0200 +++ b/src/ZF/Order.thy Wed May 08 10:14:07 2002 +0200 @@ -43,7 +43,7 @@ "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)" syntax (xsymbols) - ord_iso :: [i,i,i,i]=>i ("('(_,_') \\<cong> '(_,_'))" 50) + ord_iso :: [i,i,i,i]=>i ("(\\<langle>_, _\\<rangle> \\<cong>/ \\<langle>_, _\\<rangle>)" 51) end