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