src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
changeset 66804 3f9bb52082c4
parent 65680 378a2f11bec9
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -648,7 +648,7 @@
     1.4        if \<exists>x\<in>space M. y = f x \<and> z = g x then y * emeasure M {x\<in>space M. g x = z} else 0))"
     1.5      by (auto intro!: sum.cong simp: sum_distrib_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 "integral\<^sup>S M f = ?r" .
    1.11  qed