diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/ZF/UNITY/Increasing.thy
--- 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)"