diff -r cb34f5f49a08 -r ec32cdaab97b src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Dec 19 13:58:12 2017 +0100
@@ -808,7 +808,7 @@
   finally show ?thesis .
 qed
 
-lemma continuous_on_LINT_pmf: -- \<open>This is dominated convergence!?\<close>
+lemma continuous_on_LINT_pmf: \<comment> \<open>This is dominated convergence!?\<close>
   fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes f: "\<And>i. i \<in> set_pmf M \<Longrightarrow> continuous_on A (f i)"
     and bnd: "\<And>a i. a \<in> A \<Longrightarrow> i \<in> set_pmf M \<Longrightarrow> norm (f i a) \<le> B"