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/UNITY/Increasing.thy
changeset 80917 2a77bc3b4eac
parent 76217 8655344f1cf6
child 81125 ec121999a9cb 
--- a/src/ZF/UNITY/Increasing.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Increasing.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -23,7 +23,7 @@
                 (\<forall>x \<in> state. f(x):A)}"
 
 abbreviation (input)
-  IncWrt ::  "[i\<Rightarrow>i, i, i] \<Rightarrow> i" (\<open>(_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60)  where
+  IncWrt ::  "[i\<Rightarrow>i, i, i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>mixfix IncreasingWrt\<close>\<close>_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60)  where
   "f IncreasingWrt r/A \<equiv> Increasing[A](r,f)"
isabelle