src/HOL/Probability/Convolution.thy
changeset 57512 cc97b347b301
parent 57235 b0b9a10e4bf4
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Probability/Convolution.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Probability/Convolution.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4    apply (subst nn_integral_indicator[symmetric], simp)
     1.5    apply (subst nn_integral_convolution, 
     1.6          auto intro!: borel_measurable_indicator borel_measurable_indicator' convolution_finite)+
     1.7 -  by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add_assoc)
     1.8 +  by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add.assoc)
     1.9  
    1.10  lemma convolution_emeasure_3':
    1.11    assumes [simp, measurable]:"A \<in> sets borel"
    1.12 @@ -96,7 +96,7 @@
    1.13    have "emeasure (M \<star> N) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator A (x + y) \<partial>N \<partial>M" by (auto intro!: convolution_emeasure')
    1.14    also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. (\<lambda>(x,y). indicator A (x + y)) (x, y) \<partial>N \<partial>M" by (auto intro!: nn_integral_cong)
    1.15    also have "... = \<integral>\<^sup>+y. \<integral>\<^sup>+x. (\<lambda>(x,y). indicator A (x + y)) (x, y) \<partial>M \<partial>N" by (rule Fubini[symmetric]) simp
    1.16 -  also have "... = emeasure (N \<star> M) A" by (auto intro!: nn_integral_cong simp: add_commute convolution_emeasure')
    1.17 +  also have "... = emeasure (N \<star> M) A" by (auto intro!: nn_integral_cong simp: add.commute convolution_emeasure')
    1.18    finally show "emeasure (M \<star> N) A = emeasure (N \<star> M) A" by simp
    1.19  qed
    1.20