--- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Apr 24 13:31:52 2010 -0700
@@ -2181,7 +2181,7 @@
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})"