# HG changeset patch
# User paulson
# Date 1020845647 -7200
# Node ID 6f7526467e5ad15d4e884a329349be21c3333daa
# Parent  336b0bcbd27cbd746099b49029b773eb6d6a1f52
better xsymbol syntax

diff -r 336b0bcbd27c -r 6f7526467e5a 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