# HG changeset patch
# User wenzelm
# Date 1444509897 -7200
# Node ID 045b4d7a53e291410bd1e64a4bf4ef365eea643f
# Parent  808222c1cf662ef9efab04a95c27d1037e661987
tuned syntax -- more symbols;

diff -r 808222c1cf66 -r 045b4d7a53e2 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Sat Oct 10 22:44:45 2015 +0200
+++ b/src/ZF/Order.thy	Sat Oct 10 22:44:57 2015 +0200
@@ -49,8 +49,8 @@
               {f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longrightarrow> <f`x,f`y>:s}"
 
 definition
-  ord_iso  :: "[i,i,i,i]=>i"            (*Order isomorphisms*)  where
-   "ord_iso(A,r,B,s) ==
+  ord_iso  :: "[i,i,i,i]=>i"  ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)  (*Order isomorphisms*)  where
+   "\<langle>A,r\<rangle> \<cong> \<langle>B,s\<rangle> ==
               {f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
 
 definition
@@ -66,11 +66,6 @@
   first :: "[i, i, i] => o"  where
     "first(u, X, R) == u \<in> X & (\<forall>v\<in>X. v\<noteq>u \<longrightarrow> <u,v> \<in> R)"
 
-
-notation (xsymbols)
-  ord_iso  ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
-
-
 subsection\<open>Immediate Consequences of the Definitions\<close>
 
 lemma part_ord_Imp_asym: