diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Probability/SPMF.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -2621,8 +2621,9 @@
 
 subsection \<open>Try\<close>
 
-definition try_spmf :: "'a spmf \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf" (\<open>TRY _ ELSE _\<close> [0,60] 59)
-where "try_spmf p q = bind_pmf p (\<lambda>x. case x of None \<Rightarrow> q | Some y \<Rightarrow> return_spmf y)"
+definition try_spmf :: "'a spmf \<Rightarrow> 'a spmf \<Rightarrow> 'a spmf"
+  (\<open>(\<open>open_block notation=\<open>mixfix try_spmf\<close>\<close>TRY _ ELSE _)\<close> [0,60] 59)
+where "TRY p ELSE q = bind_pmf p (\<lambda>x. case x of None \<Rightarrow> q | Some y \<Rightarrow> return_spmf y)"
 
 lemma try_spmf_lossless [simp]:
   assumes "lossless_spmf p"