src/HOL/Integration.thy
changeset 33640 0d82107dc07a
parent 32960 69916a850301
     1.1 --- a/src/HOL/Integration.thy	Thu Nov 12 17:21:48 2009 +0100
     1.2 +++ b/src/HOL/Integration.thy	Thu Nov 12 17:21:51 2009 +0100
     1.3 @@ -542,7 +542,7 @@
     1.4   apply (erule subst)
     1.5   apply (subst listsum_subtractf [symmetric])
     1.6   apply (rule listsum_abs [THEN order_trans])
     1.7 - apply (subst map_compose [symmetric, unfolded o_def])
     1.8 + apply (subst map_map [unfolded o_def])
     1.9   apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
    1.10    apply (erule ssubst)
    1.11    apply (simp add: abs_minus_commute)