better xsymbol syntax
authorpaulson
Wed, 08 May 2002 10:14:07 +0200
changeset 13119 6f7526467e5a
parent 13118 336b0bcbd27c
child 13120 d1fea11b2fb6
better xsymbol syntax
src/ZF/Order.thy
--- 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