Probability: fix proof
authorhoelzl
Fri Sep 30 15:35:46 2016 +0200 (2016-09-30)
changeset 63973b09f16aeb694
parent 63972 c98d1dd7eba1
child 63974 721810140424
Probability: fix proof
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Sep 30 15:35:43 2016 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Sep 30 15:35:46 2016 +0200
     1.3 @@ -1936,7 +1936,7 @@
     1.4      by simp
     1.5    also from assms
     1.6      have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
     1.7 -    by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
     1.8 +    by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def)
     1.9    also from assms
    1.10      have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
    1.11      by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)