src/HOL/Analysis/Bochner_Integration.thy
changeset 66804 3f9bb52082c4
parent 66447 a1f5c5c26fa6
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -368,7 +368,7 @@
     1.4        if \<exists>x\<in>space M. y = f x \<and> z = g x then measure M {x\<in>space M. g x = z} *\<^sub>R y else 0))"
     1.5      by (auto intro!: sum.cong simp: scaleR_sum_left)
     1.6    also have "\<dots> = ?r"
     1.7 -    by (subst sum.commute)
     1.8 +    by (subst sum.swap)
     1.9         (auto intro!: sum.cong simp: sum.If_cases scaleR_sum_right[symmetric] eq)
    1.10    finally show "simple_bochner_integral M f = ?r" .
    1.11  qed