src/HOL/Analysis/Measure_Space.thy
changeset 68046 6aba668aea78
parent 67989 706f86afff43
child 68403 223172b97d0b
     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Wed Apr 25 21:29:02 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Thu Apr 26 19:51:32 2018 +0200
     1.3 @@ -1622,7 +1622,7 @@
     1.4      using emeasure_subadditive[OF measurable] fin
     1.5      apply simp
     1.6      apply (subst (asm) (2 3 4) emeasure_eq_ennreal_measure)
     1.7 -    apply (auto simp add: ennreal_plus[symmetric] simp del: ennreal_plus)
     1.8 +    apply (auto reorient: ennreal_plus)
     1.9      done
    1.10  qed
    1.11