src/HOL/Multivariate_Analysis/Integration.thy

   assumes "d tagged_division_of {a..b}"
   shows "setsum (\<lambda>(x,l). content l) d = content({a..b})"
   unfolding operative_tagged_division[OF monoidal_monoid operative_content assms,THEN sym]
   apply(subst setsum_iterate) using assms by auto
 
-subsection {* Finally, the integral of a constant\<forall> *}
+subsection {* Finally, the integral of a constant *}
 
 lemma has_integral_const[intro]:
   "((\<lambda>x. c) has_integral (content({a..b::real^'n}) *\<^sub>R c)) ({a..b})"
   unfolding has_integral apply(rule,rule,rule_tac x="\<lambda>x. ball x 1" in exI)
   apply(rule,rule gauge_trivial)apply(rule,rule,erule conjE)