# HG changeset patch
# User hoelzl
# Date 1475242546 -7200
# Node ID b09f16aeb694d149f06a22b824a07250c141eeeb
# Parent  c98d1dd7eba13cd7cd0e65add3765483b953aecf
Probability: fix proof

diff -r c98d1dd7eba1 -r b09f16aeb694 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Sep 30 15:35:43 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Sep 30 15:35:46 2016 +0200
@@ -1936,7 +1936,7 @@
     by simp
   also from assms
     have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
-    by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
+    by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def)
   also from assms
     have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
     by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)