Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Order.thy
changeset 80917 2a77bc3b4eac
parent 76217 8655344f1cf6 
--- a/src/ZF/Order.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Order.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -49,7 +49,7 @@
               {f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. \<langle>x,y\<rangle>:r \<longrightarrow> <f`x,f`y>:s}"
 
 definition
-  ord_iso  :: "[i,i,i,i]\<Rightarrow>i"  (\<open>(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)\<close> 51)  (*Order isomorphisms*)  where
+  ord_iso  :: "[i,i,i,i]\<Rightarrow>i"  (\<open>(\<open>notation=\<open>infix ord_iso\<close>\<close>\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)\<close> 51)  (*Order isomorphisms*)  where
    "\<langle>A,r\<rangle> \<cong> \<langle>B,s\<rangle> \<equiv>
               {f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. \<langle>x,y\<rangle>:r \<longleftrightarrow> <f`x,f`y>:s}"
isabelle