diff -r 3d89c38408cd -r de19856feb54 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 16 18:45:57 2012 +0100
@@ -483,6 +483,13 @@
   show ?thesis unfolding content_def using assms by (auto simp: *)
 qed
 
+lemma content_singleton[simp]: "content {a} = 0"
+proof -
+  have "content {a .. a} = 0"
+    by (subst content_closed_interval) auto
+  then show ?thesis by simp
+qed
+
 lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1"
 proof -
   have *: "\<forall>i<DIM('a). (0::'a)$$i \<le> (One::'a)$$i" by auto
@@ -1665,6 +1672,16 @@
   unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
   by(rule bounded_linear_scaleR_right)
 
+lemma has_integral_cmult_real:
+  fixes c :: real
+  assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
+  shows "((\<lambda>x. c * f x) has_integral c * x) A"
+proof cases
+  assume "c \<noteq> 0"
+  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
+    unfolding real_scaleR_def .
+qed simp
+
 lemma has_integral_neg:
   shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
   apply(drule_tac c="-1" in has_integral_cmul) by auto
@@ -1746,6 +1763,12 @@
   shows "f integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_cmul)
 
+lemma integrable_on_cmult_iff:
+  fixes c :: real assumes "c \<noteq> 0"
+  shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
+  using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
+  by auto
+
 lemma integrable_neg:
   shows "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_neg)
@@ -2669,6 +2692,11 @@
   unfolding split_def apply(subst scaleR_left.setsum[THEN sym, unfolded o_def])
   defer apply(subst additive_content_tagged_division[unfolded split_def]) apply assumption by auto
 
+lemma integral_const[simp]:
+  fixes a b :: "'a::ordered_euclidean_space"
+  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
+  by (rule integral_unique) (rule has_integral_const)
+
 subsection {* Bounds on the norm of Riemann sums and the integral itself. *}
 
 lemma dsum_bound: assumes "p division_of {a..b}" "norm(c) \<le> e"