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/Int.thy
changeset 81125 ec121999a9cb
parent 76215 a642599ffdea 
--- a/src/ZF/Int.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Int.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -17,8 +17,8 @@
     "int \<equiv> (nat*nat)//intrel"
 
 definition
-  int_of :: "i\<Rightarrow>i" \<comment> \<open>coercion from nat to int\<close>    (\<open>$# _\<close> [80] 80)  where
-    "$# m \<equiv> intrel `` {<natify(m), 0>}"
+  int_of :: "i\<Rightarrow>i" \<comment> \<open>coercion from nat to int\<close>  (\<open>(\<open>open_block notation=\<open>prefix $#\<close>\<close>$# _)\<close> [80] 80)
+  where "$# m \<equiv> intrel `` {<natify(m), 0>}"
 
 definition
   intify :: "i\<Rightarrow>i" \<comment> \<open>coercion from ANYTHING to int\<close>  where
@@ -29,8 +29,8 @@
     "raw_zminus(z) \<equiv> \<Union>\<langle>x,y\<rangle>\<in>z. intrel``{\<langle>y,x\<rangle>}"
 
 definition
-  zminus :: "i\<Rightarrow>i"                                 (\<open>$- _\<close> [80] 80)  where
-    "$- z \<equiv> raw_zminus (intify(z))"
+  zminus :: "i\<Rightarrow>i"  (\<open>(\<open>open_block notation=\<open>prefix $-\<close>\<close>$- _)\<close> [80] 80)
+  where "$- z \<equiv> raw_zminus (intify(z))"
 
 definition
   znegative   ::      "i\<Rightarrow>o"  where
isabelle