--- 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