src/HOL/Probability/Giry_Monad.thy

   also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
     by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
   finally show ?thesis .
 qed
 
-(* TODO: Rename. This name is too general – Manuel *)
+(* TODO: Rename. This name is too general -- Manuel *)
 lemma measurable_pair_measure:
   assumes f: "f \<in> measurable M (subprob_algebra N)"
   assumes g: "g \<in> measurable M (subprob_algebra L)"
   shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
 proof (rule measurable_subprob_algebra)