diff -r 0d82c4c94014 -r f353674c2528 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Sep 23 18:34:34 2016 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Set_Integral
-  imports Equivalence_Lebesgue_Henstock_Integration
+  imports Bochner_Integration
 begin
 
 (*
@@ -50,16 +50,10 @@
 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
 ("(2LBINT _./ _)" [0,60] 60)
 
-translations
-"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
-
 syntax
 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
 ("(3LBINT _:_./ _)" [0,60,61] 60)
 
-translations
-"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
-
 (*
     Basic properties
 *)
@@ -180,12 +174,6 @@
     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
   using assms by (simp_all add: scaleR_diff_right)
 
-lemma set_integral_reflect:
-  fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
-  shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
-  by (subst lborel_integral_real_affine[where c="-1" and t=0])
-     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
-
 (* question: why do we have this for negation, but multiplication by a constant
    requires an integrability assumption? *)
 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
@@ -528,59 +516,6 @@
 translations
 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
 
-(*
-lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x"
-  apply (simp add: norm_mult)
-  by (subst norm_mult, auto)
-*)
-
-lemma borel_integrable_atLeastAtMost':
-  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
-  assumes f: "continuous_on {a..b} f"
-  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
-  by (intro borel_integrable_compact compact_Icc f)
-
-lemma integral_FTC_atLeastAtMost:
-  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
-  assumes "a \<le> b"
-    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
-    and f: "continuous_on {a .. b} f"
-  shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
-proof -
-  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
-  have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
-    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
-  moreover
-  have "(f has_integral F b - F a) {a .. b}"
-    by (intro fundamental_theorem_of_calculus ballI assms) auto
-  then have "(?f has_integral F b - F a) {a .. b}"
-    by (subst has_integral_cong[where g=f]) auto
-  then have "(?f has_integral F b - F a) UNIV"
-    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
-  ultimately show "integral\<^sup>L lborel ?f = F b - F a"
-    by (rule has_integral_unique)
-qed
-
-lemma set_borel_integral_eq_integral:
-  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
-  assumes "set_integrable lborel S f"
-  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
-proof -
-  let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
-  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
-    by (rule has_integral_integral_lborel) fact
-  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
-    apply (subst has_integral_restrict_univ [symmetric])
-    apply (rule has_integral_eq)
-    by auto
-  thus "f integrable_on S"
-    by (auto simp add: integrable_on_def)
-  with 1 have "(f has_integral (integral S f)) S"
-    by (intro integrable_integral, auto simp add: integrable_on_def)
-  thus "LINT x : S | lborel. f x = integral S f"
-    by (intro has_integral_unique [OF 1])
-qed
-
 lemma set_borel_measurable_continuous:
   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   assumes "S \<in> sets borel" "continuous_on S f"