changeset 81995 | d67dadd69d07 |
parent 78517 | 28c1f4f5335f |
--- a/src/HOL/Probability/Giry_Monad.thy Mon Jan 27 20:29:02 2025 +0100 +++ b/src/HOL/Probability/Giry_Monad.thy Mon Jan 27 21:31:02 2025 +0100 @@ -1092,7 +1092,7 @@ "bind M f = (if space M = {} then count_space {} else join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))" -adhoc_overloading Monad_Syntax.bind bind +adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind lemma bind_empty: "space M = {} \<Longrightarrow> bind M f = count_space {}"