src/HOL/Probability/Probability_Mass_Function.thy
changeset 63918 6bf55e6e0b75
parent 63886 685fb01256af
child 63973 b09f16aeb694
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Sep 19 12:53:30 2016 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Sep 19 20:06:21 2016 +0200
     1.3 @@ -1610,7 +1610,7 @@
     1.4  
     1.5  lemma nn_integral_pmf_of_set: "nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S"
     1.6    by (subst nn_integral_measure_pmf_finite)
     1.7 -     (simp_all add: setsum_left_distrib[symmetric] card_gt_0_iff S_not_empty S_finite divide_ennreal_def
     1.8 +     (simp_all add: setsum_distrib_right[symmetric] card_gt_0_iff S_not_empty S_finite divide_ennreal_def
     1.9                  divide_ennreal[symmetric] ennreal_of_nat_eq_real_of_nat[symmetric] ennreal_times_divide)
    1.10  
    1.11  lemma integral_pmf_of_set: "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S"