--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 13:50:30 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 14:06:57 2015 +0100
@@ -282,6 +282,9 @@
using measure_pmf.emeasure_space_1 by simp
qed
+lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1"
+using measure_pmf.emeasure_space_1[of M] by simp
+
lemma in_null_sets_measure_pmfI:
"A \<inter> set_pmf p = {} \<Longrightarrow> A \<in> null_sets (measure_pmf p)"
using emeasure_eq_0_AE[where ?P="\<lambda>x. x \<in> A" and M="measure_pmf p"]