diff -r 03944a830c4a -r 6faf024a1893 src/HOL/Probability/Probability_Mass_Function.thy
--- 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"]