diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -13,7 +13,7 @@
   stay close to the developments of (finite) products \<^const>\<open>Pi\<^sub>E\<close> and their sigma-algebra
   \<^const>\<open>Pi\<^sub>M\<close>.\<close>
 
-type_notation fmap (\<open>(_ \<Rightarrow>\<^sub>F /_)\<close> [22, 21] 21)
+type_notation fmap (\<open>(\<open>notation=\<open>infix fmap\<close>\<close>_ \<Rightarrow>\<^sub>F /_)\<close> [22, 21] 21)
 
 unbundle fmap.lifting
 
@@ -25,7 +25,8 @@
 lemma finite_domain[simp, intro]: "finite (domain P)"
   by transfer simp
 
-lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a" (\<open>'((_)')\<^sub>F\<close> [0] 1000) is
+lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix proj\<close>\<close>'(_')\<^sub>F)\<close> [0] 1000) is
   "\<lambda>f x. if x \<in> dom f then the (f x) else undefined" .
 
 declare [[coercion proj]]
@@ -89,7 +90,8 @@
   "Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } "
 
 syntax
-  "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  (\<open>(3\<Pi>'' _\<in>_./ _)\<close>   10)
+  "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>'\<close>\<close>\<Pi>'' _\<in>_./ _)\<close>   10)
 syntax_consts
   "_Pi'" == Pi'
 translations
@@ -636,7 +638,8 @@
   "Pi\<^sub>F I M \<equiv> PiF I M"
 
 syntax
-  "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  (\<open>(3\<Pi>\<^sub>F _\<in>_./ _)\<close>  10)
+  "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"
+    (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>F\<close>\<close>\<Pi>\<^sub>F _\<in>_./ _)\<close>  10)
 syntax_consts
   "_PiF" == PiF
 translations