# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1502111437 -7200
# Node ID a8b89392ecb613f5551626cc72fde1d1c5e39b6b
# Parent  1f66c7d77002149f9f339136e03f2e9b1292562b# Parent  e2f426b54922f6506bab6ffe3ece47762d66866b
Merged

diff -r 1f66c7d77002 -r a8b89392ecb6 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Aug 04 18:03:50 2017 +0200
+++ b/Admin/components/components.sha1	Mon Aug 07 15:10:37 2017 +0200
@@ -34,6 +34,7 @@
 e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
 b98a98025d1f7e560ca6864a53296137dae736b4  e-1.6.tar.gz
 c11b25c919e2ec44fe2b6ac2086337b456344e97  e-1.8.tar.gz
+6b962a6b4539b7ca4199977973c61a8c98a492e8  e-2.0.tar.gz
 6d34b18ca0aa1e10bab6413045d079188c0e2dfb  exec_process-1.0.1.tar.gz
 8b9bffd10e396d965e815418295f2ee2849bea75  exec_process-1.0.2.tar.gz
 e6aada354da11e533af2dee3dcdd96c06479b053  exec_process-1.0.3.tar.gz
diff -r 1f66c7d77002 -r a8b89392ecb6 Admin/components/main
--- a/Admin/components/main	Fri Aug 04 18:03:50 2017 +0200
+++ b/Admin/components/main	Mon Aug 07 15:10:37 2017 +0200
@@ -2,7 +2,7 @@
 bash_process-1.2.1
 csdp-6.x
 cvc4-1.5
-e-1.8
+e-2.0
 isabelle_fonts-20160830
 jdk-8u131
 jedit_build-20170319
diff -r 1f66c7d77002 -r a8b89392ecb6 NEWS
--- a/NEWS	Fri Aug 04 18:03:50 2017 +0200
+++ b/NEWS	Mon Aug 07 15:10:37 2017 +0200
@@ -116,6 +116,11 @@
 
 *** HOL ***
 
+* Command and antiquotation "value" with modified default strategy:
+terms without free variables are always evaluated using plain evaluation
+only, with no fallback on normalization by evaluation.
+Minor INCOMPATIBILITY.
+
 * Notions of squarefreeness, n-th powers, and prime powers in
 HOL-Computational_Algebra and HOL-Number_Theory.
 
diff -r 1f66c7d77002 -r a8b89392ecb6 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Aug 07 15:10:37 2017 +0200
@@ -197,8 +197,8 @@
 for Alt-Ergo, set the
 environment variable \texttt{WHY3\_HOME} to the directory that contains the
 \texttt{why3} executable.
-Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 1.8,
-LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 3.0.%
+Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0,
+LEO-II 1.3.4, Satallax 2.2 to 2.7, SPASS 3.8ds, and Vampire 0.6 to 4.0.%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
 reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
 recent than 9.0 or 11.5.}%
@@ -206,7 +206,7 @@
 versions might not work well with Sledgehammer. Ideally,
 you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``3.0'').
+\texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0'').
 
 Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
 variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/ATP.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Automatic Theorem Provers (ATPs)\<close>
 
 theory ATP
-imports Meson
+  imports Meson
 begin
 
 subsection \<open>ATP problems and proofs\<close>
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -1,30 +1,13 @@
 (*  Title:      HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
     Author:     Johannes Hölzl, TU München
     Author:     Robert Himmelmann, TU München
+    Huge cleanup by LCP
 *)
 
 theory Equivalence_Lebesgue_Henstock_Integration
   imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
 begin
 
-lemma finite_product_dependent: (*FIXME DELETE*)
-  assumes "finite s"
-    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
-  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
-  using assms
-proof induct
-  case (insert x s)
-  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
-    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
-  show ?case
-    unfolding *
-    apply (rule finite_UnI)
-    using insert
-    apply auto
-    done
-qed auto
-
-
 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
   by (auto intro: order_trans)
 
@@ -90,7 +73,7 @@
   obtain d
     where "gauge d"
       and integral_f: "\<forall>p. p tagged_division_of cbox x y \<and> d fine p \<longrightarrow>
-        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - I) < e"
+        norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R f x) - I) < e"
     using \<open>0<e\<close> f unfolding has_integral by auto
 
   define C where "C X m = X \<inter> {x. ball x (1/Suc m) \<subseteq> d x}" for X m
@@ -194,14 +177,14 @@
         then show "\<Union>{k. \<exists>x. (x, k) \<in> ?p} = cbox x y"
           using p(1) by auto
       qed
-      ultimately have I: "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - I) < e"
+      ultimately have I: "norm ((\<Sum>(x,k) \<in> ?p. content k *\<^sub>R f x) - I) < e"
         using integral_f by auto
 
-      have "(\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) =
-        (\<Sum>(x, k)\<in>?T ` (p \<inter> s). content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p - s. content k *\<^sub>R f x)"
+      have "(\<Sum>(x,k) \<in> ?p. content k *\<^sub>R f x) =
+        (\<Sum>(x,k) \<in> ?T ` (p \<inter> s). content k *\<^sub>R f x) + (\<Sum>(x,k) \<in> p - s. content k *\<^sub>R f x)"
         using p(1)[THEN tagged_division_ofD(1)]
         by (safe intro!: sum.union_inter_neutral) (auto simp: s_def T_def)
-      also have "(\<Sum>(x, k)\<in>?T ` (p \<inter> s). content k *\<^sub>R f x) = (\<Sum>(x, k)\<in>p \<inter> s. content k *\<^sub>R f (T X k))"
+      also have "(\<Sum>(x,k) \<in> ?T ` (p \<inter> s). content k *\<^sub>R f x) = (\<Sum>(x,k) \<in> p \<inter> s. content k *\<^sub>R f (T X k))"
       proof (subst sum.reindex_nontrivial, safe)
         fix x1 x2 k assume 1: "(x1, k) \<in> p" "(x1, k) \<in> s" and 2: "(x2, k) \<in> p" "(x2, k) \<in> s"
           and eq: "content k *\<^sub>R f (T X k) \<noteq> 0"
@@ -209,8 +192,8 @@
         show "x1 = x2"
           by (auto simp: content_eq_0_interior)
       qed (use p in \<open>auto intro!: sum.cong\<close>)
-      finally have eq: "(\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) =
-        (\<Sum>(x, k)\<in>p \<inter> s. content k *\<^sub>R f (T X k)) + (\<Sum>(x, k)\<in>p - s. content k *\<^sub>R f x)" .
+      finally have eq: "(\<Sum>(x,k) \<in> ?p. content k *\<^sub>R f x) =
+        (\<Sum>(x,k) \<in> p \<inter> s. content k *\<^sub>R f (T X k)) + (\<Sum>(x,k) \<in> p - s. content k *\<^sub>R f x)" .
 
       have in_T: "(x, k) \<in> s \<Longrightarrow> T X k \<in> X" for x k
         using in_s[of x k] by (auto simp: C_def)
@@ -224,7 +207,7 @@
     have [simp]: "finite p"
       using tagged_division_ofD(1)[OF p(1)] .
 
-    have "(M - 3*e) * (b - a) \<le> (\<Sum>(x, k)\<in>p \<inter> s. content k) * (b - a)"
+    have "(M - 3*e) * (b - a) \<le> (\<Sum>(x,k) \<in> p \<inter> s. content k) * (b - a)"
     proof (intro mult_right_mono)
       have fin: "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}}) < \<infinity>" for X
         using \<open>?\<mu> E < \<infinity>\<close> by (rule le_less_trans[rotated]) (auto intro!: emeasure_mono \<open>E \<in> sets ?L\<close>)
@@ -287,15 +270,15 @@
       finally show "M - 3 * e \<le> (\<Sum>(x, y)\<in>p \<inter> s. content y)"
         using \<open>0 < e\<close> by (simp add: split_beta)
     qed (use \<open>a < b\<close> in auto)
-    also have "\<dots> = (\<Sum>(x, k)\<in>p \<inter> s. content k * (b - a))"
+    also have "\<dots> = (\<Sum>(x,k) \<in> p \<inter> s. content k * (b - a))"
       by (simp add: sum_distrib_right split_beta')
-    also have "\<dots> \<le> (\<Sum>(x, k)\<in>p \<inter> s. content k * (f (T ?F k) - f (T ?E k)))"
+    also have "\<dots> \<le> (\<Sum>(x,k) \<in> p \<inter> s. content k * (f (T ?F k) - f (T ?E k)))"
       using parts(3) by (auto intro!: sum_mono mult_left_mono diff_mono)
-    also have "\<dots> = (\<Sum>(x, k)\<in>p \<inter> s. content k * f (T ?F k)) - (\<Sum>(x, k)\<in>p \<inter> s. content k * f (T ?E k))"
+    also have "\<dots> = (\<Sum>(x,k) \<in> p \<inter> s. content k * f (T ?F k)) - (\<Sum>(x,k) \<in> p \<inter> s. content k * f (T ?E k))"
       by (auto intro!: sum.cong simp: field_simps sum_subtractf[symmetric])
-    also have "\<dots> = (\<Sum>(x, k)\<in>?B. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>?A. content k *\<^sub>R f x)"
+    also have "\<dots> = (\<Sum>(x,k) \<in> ?B. content k *\<^sub>R f x) - (\<Sum>(x,k) \<in> ?A. content k *\<^sub>R f x)"
       by (subst (1 2) parts) auto
-    also have "\<dots> \<le> norm ((\<Sum>(x, k)\<in>?B. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>?A. content k *\<^sub>R f x))"
+    also have "\<dots> \<le> norm ((\<Sum>(x,k) \<in> ?B. content k *\<^sub>R f x) - (\<Sum>(x,k) \<in> ?A. content k *\<^sub>R f x))"
       by auto
     also have "\<dots> \<le> e + e"
       using parts(1)[of ?E] parts(1)[of ?F] by (intro norm_diff_triangle_le[of _ I]) auto
@@ -574,11 +557,14 @@
   shows "integral\<^sup>N lborel f = I"
 proof -
   from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
-  from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
+  from borel_measurable_implies_simple_function_sequence'[OF this] 
+  obtain F where F: "\<And>i. simple_function lborel (F i)" "incseq F" 
+                 "\<And>i x. F i x < top" "\<And>x. (SUP i. F i x) = ennreal (f x)"
+    by blast
+  then have [measurable]: "\<And>i. F i \<in> borel_measurable lborel"
+    by (metis borel_measurable_simple_function)
   let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"
 
-  note F(1)[THEN borel_measurable_simple_function, measurable]
-
   have "0 \<le> I"
     using I by (rule has_integral_nonneg) (simp add: nonneg)
 
@@ -1199,13 +1185,13 @@
   assume "0 < e"
   have "S \<in> lmeasurable"
     using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets fmeasurableI_null_sets)
-  have e22: "0 < e / 2 / (2 * B * real DIM('M)) ^ DIM('N)"
+  have e22: "0 < e/2 / (2 * B * real DIM('M)) ^ DIM('N)"
     using \<open>0 < e\<close> \<open>0 < B\<close> by (simp add: divide_simps)
   obtain T
     where "open T" "S \<subseteq> T" "T \<in> lmeasurable"
-      and "measure lebesgue T \<le> measure lebesgue S + e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
+      and "measure lebesgue T \<le> measure lebesgue S + e/2 / (2 * B * DIM('M)) ^ DIM('N)"
     by (rule lmeasurable_outer_open [OF \<open>S \<in> lmeasurable\<close> e22])
-  then have T: "measure lebesgue T \<le> e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
+  then have T: "measure lebesgue T \<le> e/2 / (2 * B * DIM('M)) ^ DIM('N)"
     using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets measure_eq_0_null_sets)
   have "\<exists>r. 0 < r \<and> r \<le> 1/2 \<and>
             (x \<in> S \<longrightarrow> (\<forall>y. norm(y - x) < r
@@ -1286,7 +1272,7 @@
   qed
   have countbl: "countable (fbx ` \<D>)"
     using \<open>countable \<D>\<close> by blast
-  have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> e / 2" if "\<D>' \<subseteq> \<D>" "finite \<D>'" for \<D>'
+  have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> e/2" if "\<D>' \<subseteq> \<D>" "finite \<D>'" for \<D>'
   proof -
     have BM_ge0: "0 \<le> B * (DIM('M) * prj1 (vf X - uf X))" if "X \<in> \<D>'" for X
       using \<open>0 < B\<close> \<open>\<D>' \<subseteq> \<D>\<close> that vu_pos by fastforce
@@ -1330,7 +1316,7 @@
     qed
     also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * sum (measure lebesgue) \<D>'"
       by (simp add: sum_distrib_left)
-    also have "\<dots> \<le> e / 2"
+    also have "\<dots> \<le> e/2"
     proof -
       have div: "\<D>' division_of \<Union>\<D>'"
         apply (auto simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
@@ -1363,13 +1349,13 @@
         using \<open>0 < B\<close>
         apply (simp add: algebra_simps)
         done
-      also have "\<dots> \<le> e / 2"
+      also have "\<dots> \<le> e/2"
         using T \<open>0 < B\<close> by (simp add: field_simps)
       finally show ?thesis .
     qed
     finally show ?thesis .
   qed
-  then have e2: "sum (measure lebesgue) \<G> \<le> e / 2" if "\<G> \<subseteq> fbx ` \<D>" "finite \<G>" for \<G>
+  then have e2: "sum (measure lebesgue) \<G> \<le> e/2" if "\<G> \<subseteq> fbx ` \<D>" "finite \<G>" for \<G>
     by (metis finite_subset_image that)
   show "\<exists>W\<in>lmeasurable. f ` S \<subseteq> W \<and> measure lebesgue W < e"
   proof (intro bexI conjI)
@@ -1602,7 +1588,7 @@
   finally show "(\<Sum>k\<in>d. norm (integral k f)) \<le> integral UNIV (\<lambda>x. norm (f x))" .
 qed
 
-lemma helplemma:
+lemma absdiff_norm_less:
   assumes "sum (\<lambda>x. norm (f x - g x)) s < e"
     and "finite s"
   shows "\<bar>sum (\<lambda>x. norm(f x)) s - sum (\<lambda>x. norm(g x)) s\<bar> < e"
@@ -1613,28 +1599,27 @@
   apply (rule norm_triangle_ineq3)
   done
 
-text\<open>FIXME: needs refactoring and use of Sigma\<close>
-lemma bounded_variation_absolutely_integrable_interval:
+proposition bounded_variation_absolutely_integrable_interval:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes f: "f integrable_on cbox a b"
-    and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> sum (\<lambda>k. norm(integral k f)) d \<le> B"
+    and *: "\<And>d. d division_of (cbox a b) \<Longrightarrow> sum (\<lambda>K. norm(integral K f)) d \<le> B"
   shows "f absolutely_integrable_on cbox a b"
 proof -
-  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}"
+  let ?f = "\<lambda>d. \<Sum>K\<in>d. norm (integral K f)" and ?D = "{d. d division_of (cbox a b)}"
   have D_1: "?D \<noteq> {}"
     by (rule elementary_interval[of a b]) auto
   have D_2: "bdd_above (?f`?D)"
     by (metis * mem_Collect_eq bdd_aboveI2)
   note D = D_1 D_2
   let ?S = "SUP x:?D. ?f x"
-  show ?thesis
-    apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
-    apply (subst has_integral[of _ ?S])
-    apply safe
-  proof goal_cases
-    case e: (1 e)
-    then have "?S - e / 2 < ?S" by simp
-    then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
+  have *: "\<exists>\<gamma>. gauge \<gamma> \<and>
+             (\<forall>p. p tagged_division_of cbox a b \<and>
+                  \<gamma> fine p \<longrightarrow>
+                  norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - ?S) < e)"
+    if e: "e > 0" for e
+  proof -
+    have "?S - e/2 < ?S" using \<open>e > 0\<close> by simp
+    then obtain d where d: "d division_of (cbox a b)" "?S - e/2 < (\<Sum>k\<in>d. norm (integral k f))"
       unfolding less_cSUP_iff[OF D] by auto
     note d' = division_ofD[OF this(1)]
 
@@ -1642,126 +1627,118 @@
     proof
       fix x
       have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
-        apply (rule separate_point_closed)
-        apply (rule closed_Union)
-        apply (rule finite_subset[OF _ d'(1)])
-        using d'(4)
-        apply auto
-        done
+      proof (rule separate_point_closed)
+        show "closed (\<Union>{i \<in> d. x \<notin> i})"
+          apply (rule closed_Union)
+           apply (simp add: d'(1))
+          using d'(4) apply auto
+          done
+        show "x \<notin> \<Union>{i \<in> d. x \<notin> i}"
+          by auto
+      qed 
       then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
         by force
     qed
-    then obtain k where k: "\<And>x. 0 < k x"
-                       "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> i = {}"
+    then obtain k where k: "\<And>x. 0 < k x" "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> i = {}"
       by metis
     have "e/2 > 0"
       using e by auto
-    from henstock_lemma[OF assms(1) this] 
-    obtain g where g: "gauge g"
-          "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; g fine p\<rbrakk> 
-                \<Longrightarrow> (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+    with henstock_lemma[OF f] 
+    obtain \<gamma> where g: "gauge \<gamma>"
+      "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; \<gamma> fine p\<rbrakk> 
+                \<Longrightarrow> (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
       by (metis (no_types, lifting))      
-    let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
-    show ?case
-      apply (rule_tac x="?g" in exI)
-      apply safe
-    proof -
+    let ?g = "\<lambda>x. \<gamma> x \<inter> ball x (k x)"
+    show ?thesis 
+    proof (intro exI conjI allI impI)
       show "gauge ?g"
-        using g(1) k(1)
-        unfolding gauge_def
-        by auto
+        using g(1) k(1) by (auto simp: gauge_def)
+    next
       fix p
-      assume "p tagged_division_of (cbox a b)" and "?g fine p"
-      note p = this(1) conjunctD2[OF this(2)[unfolded fine_Int]]
+      assume "p tagged_division_of (cbox a b) \<and> ?g fine p"
+      then have p: "p tagged_division_of cbox a b" "\<gamma> fine p" "(\<lambda>x. ball x (k x)) fine p"
+        by (auto simp: fine_Int)
       note p' = tagged_division_ofD[OF p(1)]
       define p' where "p' = {(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}"
-      have gp': "g fine p'"
-        using p(2)
-        unfolding p'_def fine_def
-        by auto
+      have gp': "\<gamma> fine p'"
+        using p(2) by (auto simp: p'_def fine_def)
       have p'': "p' tagged_division_of (cbox a b)"
-        apply (rule tagged_division_ofI)
-      proof -
+      proof (rule tagged_division_ofI)
         show "finite p'"
-          apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
-            {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
-          unfolding p'_def
-          defer
-          apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
-          apply safe
-          unfolding image_iff
-          apply (rule_tac x="(i,x,l)" in bexI)
-          apply auto
-          done
-        fix x k
-        assume "(x, k) \<in> p'"
-        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
+        proof (rule finite_subset)
+          show "p' \<subseteq> (\<lambda>(k, x, l). (x, k \<inter> l)) ` (d \<times> p)"
+            by (force simp: p'_def image_iff)
+          show "finite ((\<lambda>(k, x, l). (x, k \<inter> l)) ` (d \<times> p))"
+            by (simp add: d'(1) p'(1))
+        qed
+      next
+        fix x K
+        assume "(x, K) \<in> p'"
+        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> K = i \<inter> l"
           unfolding p'_def by auto
-        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "k = i \<inter> l" by blast
-        show "x \<in> k" and "k \<subseteq> cbox a b"
+        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l" by blast
+        show "x \<in> K" and "K \<subseteq> cbox a b"
           using p'(2-3)[OF il(3)] il by auto
-        show "\<exists>a b. k = cbox a b"
+        show "\<exists>a b. K = cbox a b"
           unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
-          apply safe
-          unfolding Int_interval
-          apply auto
-          done
+          by (meson Int_interval)
       next
-        fix x1 k1
-        assume "(x1, k1) \<in> p'"
-        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
+        fix x1 K1
+        assume "(x1, K1) \<in> p'"
+        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> K1 = i \<inter> l"
           unfolding p'_def by auto
-        then obtain i1 l1 where il1: "x1 \<in> i1" "i1 \<in> d" "(x1, l1) \<in> p" "k1 = i1 \<inter> l1" by blast
-        fix x2 k2
-        assume "(x2,k2)\<in>p'"
-        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
+        then obtain i1 l1 where il1: "x1 \<in> i1" "i1 \<in> d" "(x1, l1) \<in> p" "K1 = i1 \<inter> l1" by blast
+        fix x2 K2
+        assume "(x2,K2) \<in> p'"
+        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> K2 = i \<inter> l"
           unfolding p'_def by auto
-        then obtain i2 l2 where il2: "x2 \<in> i2" "i2 \<in> d" "(x2, l2) \<in> p" "k2 = i2 \<inter> l2" by blast
-        assume "(x1, k1) \<noteq> (x2, k2)"
+        then obtain i2 l2 where il2: "x2 \<in> i2" "i2 \<in> d" "(x2, l2) \<in> p" "K2 = i2 \<inter> l2" by blast
+        assume "(x1, K1) \<noteq> (x2, K2)"
         then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
-          unfolding il1 il2
-          by auto
-        then show "interior k1 \<inter> interior k2 = {}"
+          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]  by (auto simp: il1 il2)
+        then show "interior K1 \<inter> interior K2 = {}"
           unfolding il1 il2 by auto
       next
         have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
-          unfolding p'_def using d' by auto
-        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
-          apply rule
-          apply (rule Union_least)
-          unfolding mem_Collect_eq
-          apply (erule exE)
-          apply (drule *[rule_format])
-          apply safe
+          unfolding p'_def using d' by blast
+        have "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}" if y: "y \<in> cbox a b" for y
         proof -
-          fix y
-          assume y: "y \<in> cbox a b"
-          then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
-            unfolding p'(6)[symmetric] by auto
-          then obtain x l where xl: "(x, l) \<in> p" "y \<in> l" by metis
-          then have "\<exists>k. k \<in> d \<and> y \<in> k"
+          obtain x l where xl: "(x, l) \<in> p" "y \<in> l" 
+            using y unfolding p'(6)[symmetric] by auto
+          obtain i where i: "i \<in> d" "y \<in> i" 
             using y unfolding d'(6)[symmetric] by auto
-          then obtain i where i: "i \<in> d" "y \<in> i" by metis
           have "x \<in> i"
             using fineD[OF p(3) xl(1)] using k(2) i xl by auto
-          then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
-            unfolding p'_def Union_iff
-            apply (rule_tac x="i \<inter> l" in bexI)
-            using i xl
-            apply auto
-            done
+          then show ?thesis
+            unfolding p'_def
+            by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
+        qed
+        show "\<Union>{K. \<exists>x. (x, K) \<in> p'} = cbox a b"
+        proof
+          show "\<Union>{k. \<exists>x. (x, k) \<in> p'} \<subseteq> cbox a b"
+            using * by auto
+        next
+          show "cbox a b \<subseteq> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
+          proof 
+            fix y
+            assume y: "y \<in> cbox a b"
+            obtain x L where xl: "(x, L) \<in> p" "y \<in> L" 
+              using y unfolding p'(6)[symmetric] by auto
+            obtain I where i: "I \<in> d" "y \<in> I" 
+              using y unfolding d'(6)[symmetric] by auto
+            have "x \<in> I"
+              using fineD[OF p(3) xl(1)] using k(2) i xl by auto
+            then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
+              apply (rule_tac X="I \<inter> L" in UnionI)
+              using i xl by (auto simp: p'_def)
+          qed
         qed
       qed
 
-      then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+      then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
         using g(2) gp' tagged_division_of_def by blast
-      then have **: "\<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
-        unfolding split_def
-        using p''
-        by (force intro!: helplemma)
 
-      have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
+      have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
       proof (safe, goal_cases)
         case prems: (2 _ _ x i l)
         have "x \<in> i"
@@ -1773,297 +1750,247 @@
           apply safe
           apply (rule_tac x=x in exI)
           apply (rule_tac x="i \<inter> l" in exI)
-          apply safe
-          using prems
           apply auto
           done
         then show ?case
           using prems(3) by auto
       next
-        fix x k
-        assume "(x, k) \<in> p'"
-        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
+        fix x K
+        assume "(x, K) \<in> p'"
+        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l" 
           unfolding p'_def by auto
-        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "k = i \<inter> l" by blast
-        then show "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+        then show "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
           using p'(2) by fastforce
       qed
-      have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
+      have sum_p': "(\<Sum>(x,K) \<in> p'. norm (integral K f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
         apply (subst sum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
          apply (auto intro: integral_null simp: content_eq_0_interior)
         done
-      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
+      have snd_p_div: "snd ` p division_of cbox a b"
+        by (rule division_of_tagged_division[OF p(1)])
+      note snd_p = division_ofD[OF snd_p_div]
+      have fin_d_sndp: "finite (d \<times> snd ` p)"
+        by (simp add: d'(1) snd_p(1))
 
-      have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
-        sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
+      have *: "\<And>sni sni' sf sf'. \<lbrakk>\<bar>sf' - sni'\<bar> < e/2; ?S - e/2 < sni; sni' \<le> ?S;
+                       sni \<le> sni'; sf' = sf\<rbrakk> \<Longrightarrow> \<bar>sf - ?S\<bar> < e"
         by arith
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
+      show "norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - ?S) < e"
         unfolding real_norm_def
-        apply (rule *[rule_format,OF **])
-        apply safe
-        apply(rule d(2))
-      proof goal_cases
-        case 1
-        show ?case
+      proof (rule *)
+        show "\<bar>(\<Sum>(x,K)\<in>p'. norm (content K *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e/2"
+          using p'' sum_less_e2 unfolding split_def by (force intro!: absdiff_norm_less)
+        show "(\<Sum>(x,k) \<in> p'. norm (integral k f)) \<le>?S"
           by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
-      next
-        case 2
-        have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
-          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
-          by auto
-        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
-        proof (rule sum_mono, goal_cases)
-          case k: (1 k)
-          from d'(4)[OF this] guess u v by (elim exE) note uv=this
-          define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
-          note uvab = d'(2)[OF k[unfolded uv]]
-          have "d' division_of cbox u v"
-            apply (subst d'_def)
-            apply (rule division_inter_1)
-            apply (rule division_of_tagged_division[OF p(1)])
-            apply (rule uvab)
-            done
-          then have "norm (integral k f) \<le> sum (\<lambda>k. norm (integral k f)) d'"
-            unfolding uv
-            apply (subst integral_combine_division_topdown[of _ _ d'])
-            apply (rule integrable_on_subcbox[OF assms(1) uvab])
-            apply assumption
-            apply (rule sum_norm_le)
-            apply auto
-            done
-          also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
-            apply (rule sum.mono_neutral_left)
-            apply (subst Setcompr_eq_image)
-            apply (rule finite_imageI)+
-            apply fact
-            unfolding d'_def uv
-            apply blast
-          proof (rule, goal_cases)
-            case prems: (1 i)
-            then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
-              by auto
-            from this[unfolded mem_Collect_eq] guess l .. note l=this
-            then have "cbox u v \<inter> l = {}"
-              using prems by auto
-            then show ?case
-              using l by auto
-          qed
-          also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
-            unfolding Setcompr_eq_image
-            apply (rule sum.reindex_nontrivial [unfolded o_def])
-            apply (rule finite_imageI)
-            apply (rule p')
-          proof goal_cases
-            case prems: (1 l y)
-            have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
-              apply (subst(2) interior_Int)
-              by (metis Int_lower2 Int_subset_iff interior_mono prems(4))
-            then have *: "interior (k \<inter> l) = {}"
-              using snd_p(5)[OF prems(1-3)] by auto
-            from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
-            show ?case
-              using *
-              unfolding uv Int_interval content_eq_0_interior[symmetric]
-              by auto
-          qed
-          finally show ?case .
-        qed
-        also have "\<dots> = (\<Sum>(i,l) \<in> d \<times> (snd ` p). norm (integral (i\<inter>l) f))"
-          apply (subst sum_Sigma_product[symmetric])
-          apply fact
-          using p'(1)
-          apply auto
-          done
-        also have "\<dots> = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (case_prod op \<inter> x) f))"
-          by (force simp: split_def Sigma_def intro!: sum.cong)
-        also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
-          unfolding *
-          apply (rule sum.reindex_nontrivial [symmetric, unfolded o_def])
-          apply (rule finite_product_dependent)
-          apply fact
-          apply (rule finite_imageI)
-          apply (rule p')
-          unfolding split_paired_all mem_Collect_eq split_conv o_def
+        show "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>(x,k) \<in> p'. norm (integral k f))"
         proof -
-          note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
-          fix l1 l2 k1 k2
-          assume as:
-            "(l1, k1) \<noteq> (l2, k2)"
-            "l1 \<inter> k1 = l2 \<inter> k2"
-            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
-            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
-          then have "l1 \<in> d" and "k1 \<in> snd ` p"
-            by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
-          guess u1 v1 u2 v2 by (elim exE) note uv=this
-          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
-            using as by auto
-          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-            by (metis Pair_inject \<open>k1 \<in> snd ` p\<close> \<open>l1 \<in> d\<close> as(4) d'(5) snd_p(5))
-          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
-            using as(2) by auto
-          ultimately have "interior(l1 \<inter> k1) = {}"
-            by auto
-          then show "norm (integral (l1 \<inter> k1) f) = 0"
-            unfolding uv Int_interval
-            unfolding content_eq_0_interior[symmetric]
-            by auto
-        qed
-        also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
-          unfolding sum_p'
-          apply (rule sum.mono_neutral_right)
-          apply (subst *)
-          apply (rule finite_imageI[OF finite_product_dependent])
-          apply fact
-          apply (rule finite_imageI[OF p'(1)])
-          apply safe
-        proof goal_cases
-          case (2 i ia l a b)
-          then have "ia \<inter> b = {}"
-            unfolding p'alt image_iff Bex_def not_ex
-            apply (erule_tac x="(a, ia \<inter> b)" in allE)
-            apply auto
-            done
-          then show ?case
+          have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} = (\<lambda>(k,l). k \<inter> l) ` (d \<times> snd ` p)"
             by auto
-        next
-          case (1 x a b)
-          then show ?case
-            unfolding p'_def
+          have "(\<Sum>K\<in>d. norm (integral K f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
+          proof (rule sum_mono)
+            fix K assume k: "K \<in> d"
+            from d'(4)[OF this] obtain u v where uv: "K = cbox u v" by metis
+            define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
+            have uvab: "cbox u v \<subseteq> cbox a b"
+              using d(1) k uv by blast
+            have "d' division_of cbox u v"
+              unfolding d'_def by (rule division_inter_1 [OF snd_p_div uvab])
+            moreover then have "norm (\<Sum>i\<in>d'. integral i f) \<le> (\<Sum>k\<in>d'. norm (integral k f))"
+              by (simp add: sum_norm_le)
+            ultimately have "norm (integral K f) \<le> sum (\<lambda>k. norm (integral k f)) d'"
+              apply (subst integral_combine_division_topdown[of _ _ d'])
+                apply (auto simp: uv intro: integrable_on_subcbox[OF assms(1) uvab])
+              done
+            also have "\<dots> = (\<Sum>I\<in>{K \<inter> L |L. L \<in> snd ` p}. norm (integral I f))"
+            proof -
+              have *: "norm (integral I f) = 0"
+                if "I \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
+                  "I \<notin> {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}" for I
+                using that by auto
+              show ?thesis
+                apply (rule sum.mono_neutral_left)
+                  apply (simp add: snd_p(1))
+                unfolding d'_def uv using * by auto 
+            qed
+            also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))"
+            proof -
+              have *: "norm (integral (K \<inter> l) f) = 0"
+                if "l \<in> snd ` p" "y \<in> snd ` p" "l \<noteq> y" "K \<inter> l = K \<inter> y" for l y
+              proof -
+                have "interior (K \<inter> l) \<subseteq> interior (l \<inter> y)"
+                  by (metis Int_lower2 interior_mono le_inf_iff that(4))
+                then have "interior (K \<inter> l) = {}"
+                  by (simp add: snd_p(5) that) 
+                moreover from d'(4)[OF k] snd_p(4)[OF that(1)] 
+                obtain u1 v1 u2 v2
+                  where uv: "K = cbox u1 u2" "l = cbox v1 v2" by metis
+                ultimately show ?thesis
+                  using that integral_null
+                  unfolding uv Int_interval content_eq_0_interior
+                  by (metis (mono_tags, lifting) norm_eq_zero)
+              qed
+              show ?thesis
+                unfolding Setcompr_eq_image
+                apply (rule sum.reindex_nontrivial [unfolded o_def])
+                 apply (rule finite_imageI)
+                 apply (rule p')
+                using * by auto
+            qed
+            finally show "norm (integral K f) \<le> (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))" .
+          qed
+          also have "\<dots> = (\<Sum>(i,l) \<in> d \<times> snd ` p. norm (integral (i\<inter>l) f))"
+            by (simp add: sum.cartesian_product)
+          also have "\<dots> = (\<Sum>x \<in> d \<times> snd ` p. norm (integral (case_prod op \<inter> x) f))"
+            by (force simp: split_def intro!: sum.cong)
+          also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
           proof -
-            assume "(a, b) \<in> {(x, k) |x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l}"
-            then have "\<exists>n N. (a, b) = (n, N) \<and> (\<exists>Na Nb. n \<in> Na \<and> Na \<in> d \<and> (n, Nb) \<in> p \<and> N = Na \<inter> Nb)"
-              by force
-            then show ?thesis
-              by (metis (no_types) image_iff snd_conv)
+            have eq0: " (integral (l1 \<inter> k1) f) = 0"
+              if "l1 \<inter> k1 = l2 \<inter> k2" "(l1, k1) \<noteq> (l2, k2)"
+                "l1 \<in> d" "(j1,k1) \<in> p" "l2 \<in> d" "(j2,k2) \<in> p"
+              for l1 l2 k1 k2 j1 j2
+            proof -
+              obtain u1 v1 u2 v2 where uv: "l1 = cbox u1 u2" "k1 = cbox v1 v2"
+                using \<open>(j1, k1) \<in> p\<close> \<open>l1 \<in> d\<close> d'(4) p'(4) by blast
+              have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
+                using that by auto
+              then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
+                by (meson d'(5) old.prod.inject p'(5) that(3) that(4) that(5) that(6))
+              moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
+                by (simp add: that(1))
+              ultimately have "interior(l1 \<inter> k1) = {}"
+                by auto
+              then show ?thesis
+                unfolding uv Int_interval content_eq_0_interior[symmetric] by auto
+            qed
+            show ?thesis
+              unfolding *
+              apply (rule sum.reindex_nontrivial [OF fin_d_sndp, symmetric, unfolded o_def])
+              apply clarsimp
+              by (metis eq0 fst_conv snd_conv)
           qed
+          also have "\<dots> = (\<Sum>(x,k) \<in> p'. norm (integral k f))"
+          proof -
+            have 0: "integral (ia \<inter> snd (a, b)) f = 0"
+              if "ia \<inter> snd (a, b) \<notin> snd ` p'" "ia \<in> d" "(a, b) \<in> p" for ia a b
+            proof -
+              have "ia \<inter> b = {}"
+                using that unfolding p'alt image_iff Bex_def not_ex
+                apply (erule_tac x="(a, ia \<inter> b)" in allE)
+                apply auto
+                done
+              then show ?thesis by auto
+            qed
+            have 1: "\<exists>i l. snd (a, b) = i \<inter> l \<and> i \<in> d \<and> l \<in> snd ` p" if "(a, b) \<in> p'" for a b
+              using that 
+              apply (clarsimp simp: p'_def image_iff)
+              by (metis (no_types, hide_lams) snd_conv)
+            show ?thesis
+              unfolding sum_p'
+              apply (rule sum.mono_neutral_right)
+                apply (metis * finite_imageI[OF fin_d_sndp])
+              using 0 1 by auto
+          qed
+          finally show ?thesis .
         qed
-        finally show ?case .
-      next
-        case 3
-        let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
-        have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
-          apply safe
-          unfolding image_iff
-          apply (rule_tac x="((x,l),i)" in bexI)
-          apply auto
-          done
-        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
-        have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))"
-          unfolding norm_scaleR
-          apply (rule sum.mono_neutral_left)
-          apply (subst *)
-          apply (rule finite_imageI)
-          apply fact
-          unfolding p'alt
-          apply blast
-          apply safe
-          apply (rule_tac x=x in exI)
-          apply (rule_tac x=i in exI)
-          apply (rule_tac x=l in exI)
-          apply auto
-          done
-        also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
-          unfolding *
-          apply (subst sum.reindex_nontrivial)
-          apply fact
-          unfolding split_paired_all
-          unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
-          apply (elim conjE)
+        show "(\<Sum>(x,k) \<in> p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x))"
         proof -
-          fix x1 l1 k1 x2 l2 k2
-          assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
-            "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
-          from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
-          from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
-            by auto
-          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-            apply -
-            apply (erule disjE)
-            apply (rule disjI2)
-            defer
-            apply (rule disjI1)
-            apply (rule d'(5)[OF as(3-4)])
-            apply assumption
-            apply (rule p'(5)[OF as(1-2)])
-            apply auto
-            done
-          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
-            unfolding  as ..
-          ultimately have "interior (l1 \<inter> k1) = {}"
-            by auto
-          then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
-            unfolding uv Int_interval
-            unfolding content_eq_0_interior[symmetric]
-            by auto
-        qed safe
-        also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
-          apply (subst sum_Sigma_product[symmetric])
-          apply (rule p')
-          apply (rule d')
-          apply (rule sum.cong)
-          apply (rule refl)
-          unfolding split_paired_all split_conv
-        proof -
-          fix x l
-          assume as: "(x, l) \<in> p"
-          note xl = p'(2-4)[OF this]
-          from this(3) guess u v by (elim exE) note uv=this
-          have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
-            by (simp add: Int_commute uv)
-          also have "\<dots> = sum content {k \<inter> cbox u v| k. k \<in> d}"
-            unfolding Setcompr_eq_image
-            apply (rule sum.reindex_nontrivial [unfolded o_def, symmetric])
-            apply (rule d')
-          proof goal_cases
-            case prems: (1 k y)
-            from d'(4)[OF this(1)] d'(4)[OF this(2)]
-            guess u1 v1 u2 v2 by (elim exE) note uv=this
-            have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
-              apply (subst interior_Int)
-              using d'(5)[OF prems(1-3)]
-              apply auto
+          let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
+          have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
+            by force
+          have fin_pd: "finite (p \<times> d)"
+            using finite_cartesian_product[OF p'(1) d'(1)] by metis
+          have "(\<Sum>(x,k) \<in> p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x,k) \<in> ?S. \<bar>content k\<bar> * norm (f x))"
+            unfolding norm_scaleR
+            apply (rule sum.mono_neutral_left)
+              apply (subst *)
+              apply (rule finite_imageI [OF fin_pd])
+            unfolding p'alt apply auto
+            by fastforce
+          also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
+          proof -
+            have "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
+              if "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
+                "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "x1 \<noteq> x2 \<or> l1 \<noteq> l2 \<or> k1 \<noteq> k2"
+              for x1 l1 k1 x2 l2 k2
+            proof -
+              obtain u1 v1 u2 v2 where uv: "k1 = cbox u1 u2" "l1 = cbox v1 v2"
+                by (meson \<open>(x1, l1) \<in> p\<close> \<open>k1 \<in> d\<close> d(1) division_ofD(4) p'(4))
+              have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
+                using that by auto
+              then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
+                apply (rule disjE)
+                using that p'(5) d'(5) by auto
+              moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
+                unfolding that ..
+              ultimately have "interior (l1 \<inter> k1) = {}"
+                by auto
+              then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
+                unfolding uv Int_interval content_eq_0_interior[symmetric] by auto
+            qed 
+            then show ?thesis
+              unfolding *
+              apply (subst sum.reindex_nontrivial [OF fin_pd])
+              unfolding split_paired_all o_def split_def prod.inject
+               apply force+
               done
-            also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
-              by auto
-            also have "\<dots> = interior (k \<inter> cbox u v)"
-              unfolding prems(4) by auto
-            finally show ?case
-              unfolding uv Int_interval content_eq_0_interior ..
           qed
-          also have "\<dots> = sum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
-            apply (rule sum.mono_neutral_right)
-            unfolding Setcompr_eq_image
-            apply (rule finite_imageI)
-            apply (rule d')
-            apply blast
-            apply safe
-            apply (rule_tac x=k in exI)
-          proof goal_cases
-            case prems: (1 i k)
-            from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
-            have "interior (k \<inter> cbox u v) \<noteq> {}"
-              using prems(2)
-              unfolding ab Int_interval content_eq_0_interior
-              by auto
-            then show ?case
-              using prems(1)
-              using interior_subset[of "k \<inter> cbox u v"]
-              by auto
+          also have "\<dots> = (\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x))"
+          proof -
+            have sumeq: "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
+              if "(x, l) \<in> p" for x l
+            proof -
+              note xl = p'(2-4)[OF that]
+              then obtain u v where uv: "l = cbox u v" by blast
+              have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
+                by (simp add: Int_commute uv)
+              also have "\<dots> = sum content {k \<inter> cbox u v| k. k \<in> d}"
+              proof -
+                have eq0: "content (k \<inter> cbox u v) = 0"
+                  if "k \<in> d" "y \<in> d" "k \<noteq> y" and eq: "k \<inter> cbox u v = y \<inter> cbox u v" for k y
+                proof -
+                  from d'(4)[OF that(1)] d'(4)[OF that(2)]
+                  obtain \<alpha> \<beta> where \<alpha>: "k \<inter> cbox u v = cbox \<alpha> \<beta>"
+                    by (meson Int_interval)
+                  have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
+                    by (simp add: d'(5) that)
+                  also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
+                    by auto
+                  also have "\<dots> = interior (k \<inter> cbox u v)"
+                    unfolding eq by auto
+                  finally show ?thesis
+                    unfolding \<alpha> content_eq_0_interior ..
+                qed
+                then show ?thesis
+                  unfolding Setcompr_eq_image
+                  apply (rule sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
+                  by auto
+              qed
+              also have "\<dots> = sum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
+                apply (rule sum.mono_neutral_right)
+                unfolding Setcompr_eq_image
+                  apply (rule finite_imageI [OF \<open>finite d\<close>])
+                 apply (fastforce simp: inf.commute)+
+                done
+              finally show "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
+                unfolding sum_distrib_right[symmetric] real_scaleR_def
+                apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
+                using xl(2)[unfolded uv] unfolding uv apply auto
+                done
+            qed
+            show ?thesis
+              by (subst sum_Sigma_product[symmetric]) (auto intro!: sumeq sum.cong p' d')
           qed
-          finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
-            unfolding sum_distrib_right[symmetric] real_scaleR_def
-            apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
-            using xl(2)[unfolded uv]
-            unfolding uv
-            apply auto
-            done
+          finally show ?thesis .
         qed
-        finally show ?case .
-      qed
-    qed
+      qed (rule d)
+    qed 
   qed
+  then show ?thesis
+    using absolutely_integrable_onI [OF f has_integral_integrable] has_integral[of _ ?S]
+    by blast
 qed
 
+
 lemma bounded_variation_absolutely_integrable:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes "f integrable_on UNIV"
@@ -2169,43 +2096,40 @@
           using \<open>e > 0\<close> by auto
         from * [OF this] obtain d1 where
           d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
-            norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e / 2"
+            norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e/2"
           by auto
         from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
           d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
-            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
+            (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2" .
          obtain p where
           p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
           by (rule fine_division_exists [OF gauge_Int [OF d1(1) d2(1)], of a b])
             (auto simp add: fine_Int)
-        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
-          \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
+        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e/2 \<longrightarrow>
+          \<bar>sf' - di\<bar> < e/2 \<longrightarrow> di < ?S + e"
           by arith
         show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
           apply (subst if_P)
           apply rule
         proof (rule *[rule_format])
-          show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e / 2"
+          show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e/2"
             unfolding split_def
-            apply (rule helplemma)
+            apply (rule absdiff_norm_less)
             using d2(2)[rule_format,of p]
             using p(1,3)
             unfolding tagged_division_of_def split_def
             apply auto
             done
-          show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e / 2"
+          show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
             using d1(2)[rule_format,OF conjI[OF p(1,2)]]
             by (simp only: real_norm_def)
-          show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
+          show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
             apply (rule sum.cong)
             apply (rule refl)
             unfolding split_paired_all split_conv
             apply (drule tagged_division_ofD(4)[OF p(1)])
-            unfolding norm_scaleR
-            apply (subst abs_of_nonneg)
-            apply auto
-            done
-          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
+            by simp
+          show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
             using partial_division_of_tagged_division[of p "cbox a b"] p(1)
             apply (subst sum.over_tagged_division_lemma[OF p(1)])
             apply (simp add: content_eq_0_interior)
@@ -2678,11 +2602,12 @@
     using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
   then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
     by (intro tendsto_lowerbound[OF lim])
-       (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
+       (auto simp: eventually_at_top_linorder)
 
   have "(SUP i::nat. ?f i x) = ?fR x" for x
   proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
-    from reals_Archimedean2[of "x - a"] guess n ..
+    obtain n where "x - a < real n"
+      using reals_Archimedean2[of "x - a"] ..
     then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
       by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
     then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -9,6 +9,10 @@
   Lebesgue_Measure Tagged_Division
 begin
 
+lemma eps_leI: 
+  assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
+  by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl)
+
 (*FIXME DELETE*)
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
 
@@ -1260,7 +1264,7 @@
 
 lemma has_integral_separate_sides:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_integral i) (cbox a b)"
+  assumes f: "(f has_integral i) (cbox a b)"
     and "e > 0"
     and k: "k \<in> Basis"
   obtains d where "gauge d"
@@ -1268,18 +1272,23 @@
         p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow>
         norm ((sum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + sum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e"
 proof -
-  guess d using has_integralD[OF assms(1-2)] . note d=this
+  obtain \<gamma> where d: "gauge \<gamma>"
+      "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma> fine p\<rbrakk>
+            \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < e"
+    using has_integralD[OF f \<open>e > 0\<close>] by metis
   { fix p1 p2
-    assume "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1"
-    note p1=tagged_division_ofD[OF this(1)] this
-    assume "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" "d fine p2"
-    note p2=tagged_division_ofD[OF this(1)] this
-    note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this
+    assume tdiv1: "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" and "\<gamma> fine p1"
+    note p1=tagged_division_ofD[OF this(1)] 
+    assume tdiv2: "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" and "\<gamma> fine p2"
+    note p2=tagged_division_ofD[OF this(1)] 
+    note tagged_division_union_interval[OF tdiv1 tdiv2] 
+    note p12 = tagged_division_ofD[OF this] this
     { fix a b
       assume ab: "(a, b) \<in> p1 \<inter> p2"
       have "(a, b) \<in> p1"
         using ab by auto
-      with p1 obtain u v where uv: "b = cbox u v" by auto
+      obtain u v where uv: "b = cbox u v"
+        using \<open>(a, b) \<in> p1\<close> p1(4) by moura
       have "b \<subseteq> {x. x\<bullet>k = c}"
         using ab p1(3)[of a b] p2(3)[of a b] by fastforce
       moreover
@@ -1288,25 +1297,23 @@
         assume "\<not> ?thesis"
         then obtain x where x: "x \<in> interior {x::'a. x\<bullet>k = c}"
           by auto
-        then guess e unfolding mem_interior .. note e=this
+        then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> {x. x \<bullet> k = c}"
+          using mem_interior by metis
         have x: "x\<bullet>k = c"
           using x interior_subset by fastforce
-        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (e / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then e/2 else 0)"
-          using e k by (auto simp: inner_simps inner_not_same_Basis)
-        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
-              (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))"
+        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon> / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
+          using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_simps inner_not_same_Basis)
+        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon> / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
+              (\<Sum>i\<in>Basis. (if i = k then \<epsilon> / 2 else 0))"
           using "*" by (blast intro: sum.cong)
-        also have "\<dots> < e"
-          apply (subst sum.delta)
-          using e
-          apply auto
-          done
-        finally have "x + (e/2) *\<^sub>R k \<in> ball x e"
+        also have "\<dots> < \<epsilon>"
+          by (subst sum.delta) (use \<open>0 < \<epsilon>\<close> in auto)
+        finally have "x + (\<epsilon>/2) *\<^sub>R k \<in> ball x \<epsilon>"
           unfolding mem_ball dist_norm by(rule le_less_trans[OF norm_le_l1])
-        then have "x + (e/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}"
-          using e by auto
+        then have "x + (\<epsilon>/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}"
+          using \<epsilon> by auto
         then show False
-          unfolding mem_Collect_eq using e x k by (auto simp: inner_simps)
+          using \<open>0 < \<epsilon>\<close> x k by (auto simp: inner_simps)
       qed
       ultimately have "content b = 0"
         unfolding uv content_eq_0_interior
@@ -1318,11 +1325,11 @@
                norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
       by (subst sum.union_inter_neutral) (auto simp: p1 p2)
     also have "\<dots> < e"
-      by (rule k d(2) p12 fine_Un p1 p2)+
+      using d(2) p12 by (simp add: fine_Un k \<open>\<gamma> fine p1\<close> \<open>\<gamma> fine p2\<close>)
     finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" .
    }
   then show ?thesis
-    by (auto intro: that[of d] d elim: )
+    using d(1) that by auto
 qed
 
 lemma integrable_split [intro]:
@@ -2463,53 +2470,39 @@
 proof safe
   fix a b :: 'b
   show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-    if "box a b = {}"
+    if "box a b = {}" for a b
     apply (rule_tac x=f in exI)
-    using assms that
-    apply (auto simp: content_eq_0_interior)
-    done
+    using assms that by (auto simp: content_eq_0_interior)
   {
-    fix c g
-    fix k :: 'b
-    assume as: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
+    fix c g and k :: 'b
+    assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
     assume k: "k \<in> Basis"
     show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-      "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
-      apply (rule_tac[!] x=g in exI)
-      using as(1) integrable_split[OF as(2) k]
-      apply auto
-      done
+         "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
+       apply (rule_tac[!] x=g in exI)
+      using fg integrable_split[OF g k] by auto
   }
-  fix c k g1 g2
-  assume as: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-    "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
-  assume k: "k \<in> Basis"
-  let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
   show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-    apply (rule_tac x="?g" in exI)
-    apply safe
-  proof goal_cases
-    case (1 x)
-    then show ?case
-      apply -
-      apply (cases "x\<bullet>k=c")
-      apply (case_tac "x\<bullet>k < c")
-      using as assms
-      apply auto
-      done
-  next
-    case 2
-    presume "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-      and "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-    then guess h1 h2 unfolding integrable_on_def by auto
-    from has_integral_split[OF this k] show ?case
-      unfolding integrable_on_def by auto
-  next
-    show "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-      apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]])
-      using k as(2,4)
-      apply auto
-      done
+    if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" 
+      and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+      and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" 
+      and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" 
+      and k: "k \<in> Basis"
+    for c k g1 g2
+  proof -
+    let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+    show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+    proof (intro exI conjI ballI)
+      show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
+        by (auto simp: that assms fg1 fg2)
+      show "?g integrable_on cbox a b"
+      proof -
+        have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
+          by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
+        with has_integral_split[OF _ _ k] show ?thesis
+          unfolding integrable_on_def by blast
+      qed
+    qed
   qed
 qed
 
@@ -2524,18 +2517,16 @@
 lemma approximable_on_division:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
   assumes "0 \<le> e"
-    and "d division_of (cbox a b)"
-    and "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
+    and d: "d division_of (cbox a b)"
+    and f: "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
   obtains g where "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
 proof -
-  note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_approximable[OF assms(1)] assms(2)]
-  from assms(3) this[unfolded comm_monoid_set_F_and, of f] division_of_finite[OF assms(2)]
-  guess g by auto
-  then show thesis
-    apply -
-    apply (rule that[of g])
-    apply auto
-    done
+  note * = comm_monoid_set.operative_division
+             [OF comm_monoid_set_and operative_approximable[OF \<open>0 \<le> e\<close>] d]
+  have "finite d"
+    by (rule division_of_finite[OF d])
+  with f *[unfolded comm_monoid_set_F_and, of f] that show thesis
+    by auto
 qed
 
 lemma integrable_continuous:
@@ -2669,18 +2660,22 @@
 lemma fundamental_theorem_of_calculus:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes "a \<le> b"
-    and "\<forall>x\<in>{a .. b}. (f has_vector_derivative f' x) (at x within {a .. b})"
+    and vecd: "\<forall>x\<in>{a .. b}. (f has_vector_derivative f' x) (at x within {a .. b})"
   shows "(f' has_integral (f b - f a)) {a .. b}"
   unfolding has_integral_factor_content box_real[symmetric]
 proof safe
   fix e :: real
-  assume e: "e > 0"
-  note assm = assms(2)[unfolded has_vector_derivative_def has_derivative_within_alt]
-  have *: "\<And>P Q. \<forall>x\<in>{a .. b}. P x \<and> (\<forall>e>0. \<exists>d>0. Q x e d) \<Longrightarrow> \<forall>x. \<exists>(d::real)>0. x\<in>{a .. b} \<longrightarrow> Q x e d"
-    using e by blast
-  note this[OF assm,unfolded gauge_existence_lemma]
-  from choice[OF this,unfolded Ball_def[symmetric]] guess d ..
-  note d=conjunctD2[OF this[rule_format],rule_format]
+  assume "e > 0"
+  then have "\<forall>x. \<exists>d>0.
+         x \<in> {a..b} \<longrightarrow>
+         (\<forall>y\<in>{a..b}.
+             norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e * norm (y - x))"
+    using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast
+  then obtain d where d: "\<And>x. 0 < d x"
+                 "\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; norm (y - x) < d x\<rbrakk>
+                        \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e * norm (y - x)"
+    by metis
+  
   show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
     norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b))"
     apply (rule_tac x="\<lambda>x. ball x (d x)" in exI)
@@ -2701,7 +2696,7 @@
       fix x k
       assume "(x, k) \<in> p"
       note xk = tagged_division_ofD(2-4)[OF as(1) this]
-      from this(3) guess u v by (elim exE) note k=this
+      then obtain u v where k: "k = cbox u v" by blast
       have *: "u \<le> v"
         using xk unfolding k by auto
       have ball: "\<forall>xa\<in>k. xa \<in> ball x (d x)"
@@ -2907,10 +2902,9 @@
       done
   }
   assume noteq: "{k \<in> s. content k \<noteq> 0} \<noteq> s"
-  then obtain k where k: "k \<in> s" "content k = 0"
-    by auto
-  from s(4)[OF k(1)] guess c d by (elim exE) note k=k this
-  from k have "card s > 0"
+  then obtain k c d where k: "k \<in> s" "content k = 0" "k = cbox c d"
+    using s(4) by blast
+  then have "card s > 0"
     unfolding card_gt_0_iff using assm(1) by auto
   then have card: "card (s - {k}) < card s"
     using assm(1) k(1)
@@ -2933,9 +2927,9 @@
     fix x
     fix e :: real
     assume as: "x \<in> k" "e > 0"
-    from k(2)[unfolded k content_eq_0] guess i ..
-    then have i:"c\<bullet>i = d\<bullet>i" "i\<in>Basis"
-      using s(3)[OF k(1),unfolded k] unfolding box_ne_empty by auto
+    obtain i where i: "c\<bullet>i = d\<bullet>i" "i\<in>Basis"
+      using k(2) s(3)[OF k(1)] unfolding box_ne_empty k
+      by (metis dual_order.antisym content_eq_0) 
     then have xi: "x\<bullet>i = d\<bullet>i"
       using as unfolding k mem_box by (metis antisym)
     define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
@@ -3114,42 +3108,30 @@
     f integrable_on cbox u v"
   shows "f integrable_on cbox a b"
 proof -
-  have "\<forall>x. \<exists>d. x\<in>cbox a b \<longrightarrow> d>0 \<and> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow>
+  have "\<forall>x. \<exists>d>0. x\<in>cbox a b \<longrightarrow> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow>
     f integrable_on cbox u v)"
-    using assms by auto
-  note this[unfolded gauge_existence_lemma]
-  from choice[OF this] guess d .. note d=this[rule_format]
-  guess p
-    apply (rule fine_division_exists[OF gauge_ball_dependent,of d a b])
-    using d
+    using assms by (metis zero_less_one)
+  then obtain d where d: "\<And>x. 0 < d x"
+     "\<And>x u v. \<lbrakk>x \<in> cbox a b; x \<in> cbox u v; cbox u v \<subseteq> ball x (d x); cbox u v \<subseteq> cbox a b\<rbrakk> 
+               \<Longrightarrow> f integrable_on cbox u v"
+    by metis
+  obtain p where p: "p tagged_division_of cbox a b" "(\<lambda>x. ball x (d x)) fine p"
+    using fine_division_exists[OF gauge_ball_dependent,of d a b] d(1) by blast 
+  then have sndp: "snd ` p division_of cbox a b"
+    by (metis division_of_tagged_division)
+  have "f integrable_on k" if "(x, k) \<in> p" for x k
+    using tagged_division_ofD(2-4)[OF p(1) that] fineD[OF p(2) that] d[of x] by auto
+  then show ?thesis
+    unfolding comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable sndp,  symmetric]
+              comm_monoid_set_F_and
     by auto
-  note p=this(1-2)
-  note division_of_tagged_division[OF this(1)]
-  note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable, OF this, symmetric, of f]
-  show ?thesis
-    unfolding * comm_monoid_set_F_and
-    apply safe
-    unfolding snd_conv
-  proof -
-    fix x k
-    assume "(x, k) \<in> p"
-    note tagged_division_ofD(2-4)[OF p(1) this] fineD[OF p(2) this]
-    then show "f integrable_on k"
-      apply safe
-      apply (rule d[THEN conjunct2,rule_format,of x])
-      apply (auto intro: order.trans)
-      done
-  qed
 qed
 
 
 subsection \<open>Second FTC or existence of antiderivative.\<close>
 
 lemma integrable_const[intro]: "(\<lambda>x. c) integrable_on cbox a b"
-  unfolding integrable_on_def
-  apply rule
-  apply (rule has_integral_const)
-  done
+  unfolding integrable_on_def by blast
 
 lemma integral_has_vector_derivative_continuous_at:
   fixes f :: "real \<Rightarrow> 'a::banach"
@@ -3239,22 +3221,18 @@
   assumes "continuous_on {a .. b} f"
   obtains g where "\<forall>u\<in>{a .. b}. \<forall>v \<in> {a .. b}. u \<le> v \<longrightarrow> (f has_integral (g v - g u)) {u .. v}"
 proof -
-  from antiderivative_continuous[OF assms] guess g . note g=this
-  show ?thesis
-    apply (rule that[of g])
-    apply safe
-  proof goal_cases
-    case prems: (1 u v)
+  obtain g 
+    where g: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative f x) (at x within {a..b})" 
+    using  antiderivative_continuous[OF assms] by metis
+  have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
+  proof -
     have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
-      apply rule
-      apply (rule has_vector_derivative_within_subset)
-      apply (rule g[rule_format])
-      using prems(1,2)
-      apply auto
-      done
-    then show ?case
-      using fundamental_theorem_of_calculus[OF prems(3), of g f] by auto
+      by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
+    then show ?thesis
+      by (simp add: fundamental_theorem_of_calculus that(3))
   qed
+  then show ?thesis
+    using that by blast
 qed
 
 
@@ -3268,7 +3246,7 @@
     and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
     and h: "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
     and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
-    and "(f has_integral i) (cbox a b)"
+    and intfi: "(f has_integral i) (cbox a b)"
   shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
 proof -
   show ?thesis when *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
@@ -3282,22 +3260,11 @@
       unfolding prems assms(8)[unfolded prems has_integral_empty_eq] by auto
   qed
   assume "cbox a b \<noteq> {}"
-  from assms(6)[rule_format,of a b] guess w z by (elim exE) note wz=this
+  obtain w z where wz: "h ` cbox a b = cbox w z"
+    using h by blast
   have inj: "inj g" "inj h"
-    unfolding inj_on_def
-    apply safe
-    apply(rule_tac[!] ccontr)
-    using assms(2)
-    apply(erule_tac x=x in allE)
-    using assms(2)
-    apply(erule_tac x=y in allE)
-    defer
-    using assms(3)
-    apply (erule_tac x=x in allE)
-    using assms(3)
-    apply(erule_tac x=y in allE)
-    apply auto
-    done
+    apply (metis assms(2) injI)
+    by (metis assms(3) injI)
   from h obtain ha hb where h_eq: "h ` cbox a b = cbox ha hb" by blast
   show ?thesis
     unfolding h_eq has_integral
@@ -3305,12 +3272,17 @@
   proof safe
     fix e :: real
     assume e: "e > 0"
-    with assms(1) have "e * r > 0" by simp
-    from assms(8)[unfolded has_integral,rule_format,OF this] guess d by (elim exE conjE) note d=this[rule_format]
+    with \<open>0 < r\<close> have "e * r > 0" by simp
+    with intfi[unfolded has_integral]
+    obtain d where d: "gauge d"
+                   "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
+                        \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < e * r" 
+      by metis
     define d' where "d' x = {y. g y \<in> d (g x)}" for x
     have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
       unfolding d'_def ..
-    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
+    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p 
+              \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
     proof (rule_tac x=d' in exI, safe)
       show "gauge d'"
         using d(1)
@@ -3377,16 +3349,10 @@
         assume "x \<in> cbox a b"
         then have "h x \<in>  \<Union>{k. \<exists>x. (x, k) \<in> p}"
           using p(6) by auto
-        then guess X unfolding Union_iff .. note X=this
-        from this(1) guess y unfolding mem_Collect_eq ..
+        then obtain X y where "h x \<in> X" "(y, X) \<in> p" by blast
         then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}"
-          apply -
-          apply (rule_tac X="g ` X" in UnionI)
-          defer
-          apply (rule_tac x="h x" in image_eqI)
-          using X(2) assms(3)[rule_format,of x]
-          apply auto
-          done
+          apply (clarsimp simp: )
+          by (metis (no_types, lifting) assms(3) image_eqI pair_imageI)
       qed
         note ** = d(2)[OF this]
         have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
@@ -3626,8 +3592,8 @@
 lemma fundamental_theorem_of_calculus_interior:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a \<le> b"
-    and "continuous_on {a .. b} f"
-    and "\<forall>x\<in>{a <..< b}. (f has_vector_derivative f'(x)) (at x)"
+    and contf: "continuous_on {a .. b} f"
+    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
   shows "(f' has_integral (f b - f a)) {a .. b}"
 proof -
   {
@@ -3655,29 +3621,30 @@
   { presume "\<And>e. e > 0 \<Longrightarrow> ?P e" then show ?thesis unfolding has_integral_factor_content_real by auto }
   fix e :: real
   assume e: "e > 0"
-  note assms(3)[unfolded has_vector_derivative_def has_derivative_at_alt ball_conj_distrib]
-  note conjunctD2[OF this]
-  note bounded=this(1) and this(2)
-  from this(2) have "\<forall>x\<in>box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
-    norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
-    apply -
-    apply safe
-    apply (erule_tac x=x in ballE)
-    apply (erule_tac x="e/2" in allE)
-    using e
-    apply auto
-    done
-  note this[unfolded bgauge_existence_lemma]
-  from choice[OF this] guess d ..
-  note conjunctD2[OF this[rule_format]]
-  note d = this[rule_format]
+  note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
+  have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
+    using derf_exp by simp
+  have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
+       (is "\<forall>x \<in> box a b. ?Q x")
+  proof
+    fix x assume x: "x \<in> box a b"
+    show "?Q x"
+      apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
+      using x e by auto
+  qed
+  from this [unfolded bgauge_existence_lemma]
+  obtain d where d: "\<And>x. 0 < d x"
+     "\<And>x y. \<lbrakk>x \<in> box a b; norm (y - x) < d x\<rbrakk>
+               \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e / 2 * norm (y - x)"
+    by metis
   have "bounded (f ` cbox a b)"
     apply (rule compact_imp_bounded compact_continuous_image)+
     using compact_cbox assms
     apply auto
     done
-  from this[unfolded bounded_pos] guess B .. note B = this[rule_format]
-
+  from this[unfolded bounded_pos] obtain B 
+    where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B"
+    by metis
   have "\<exists>da. 0 < da \<and> (\<forall>c. a \<le> c \<and> {a .. c} \<subseteq> {a .. b} \<and> {a .. c} \<subseteq> ball a da \<longrightarrow>
     norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4)"
   proof -
@@ -3700,7 +3667,7 @@
         apply (auto simp add: field_simps)
         done
     qed
-    then guess l .. note l = conjunctD2[OF this]
+    then obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b - a) / 8" by metis
     show ?thesis
       apply (rule_tac x="min k l" in exI)
       apply safe
@@ -3715,24 +3682,28 @@
         by (rule norm_triangle_ineq4)
       also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
       proof (rule add_mono)
-        have "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
-          using as' by auto
-        then show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8"
-          apply -
-          apply (rule order_trans[OF _ l(2)])
+        have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
           unfolding norm_scaleR
           apply (rule mult_right_mono)
-          apply auto
-          done
+          using as' by auto
+        also have "... \<le> e * (b - a) / 8"
+          by (rule l)
+        finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8" .
       next
-        show "norm (f c - f a) \<le> e * (b - a) / 8"
-          apply (rule less_imp_le)
-          apply (cases "a = c")
-          defer
-          apply (rule k(2)[unfolded dist_norm])
-          using as' e ab
-          apply (auto simp add: field_simps)
-          done
+        have "norm (f c - f a) < e * (b - a) / 8"
+        proof (cases "a = c")
+          case True
+          then show ?thesis
+            using \<open>0 < e * (b - a) / 8\<close> by auto
+        next
+          case False
+          show ?thesis
+            apply (rule k(2)[unfolded dist_norm])
+            using as' False
+             apply (auto simp add: field_simps)
+            done
+        qed
+        then show "norm (f c - f a) \<le> e * (b - a) / 8" by simp
       qed
       finally show "norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
         unfolding content_real[OF as(1)] by auto
@@ -3748,20 +3719,23 @@
     note assms(2)[unfolded continuous_on_eq_continuous_within,rule_format,OF this]
     note * = this[unfolded continuous_within Lim_within,rule_format] have "(e * (b - a)) / 8 > 0"
       using e ab by (auto simp add: field_simps)
-    from *[OF this] guess k .. note k = conjunctD2[OF this,rule_format]
-    have "\<exists>l. 0 < l \<and> norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
+    from *[OF this] obtain k
+      where k: "0 < k"
+               "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < dist x b \<and> dist x b < k\<rbrakk>
+                    \<Longrightarrow> dist (f x) (f b) < e * (b - a) / 8"
+      by blast
+    obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
     proof (cases "f' b = 0")
       case True
-      thus ?thesis using ab e by auto
+      thus ?thesis using ab e that by auto
     next
       case False
       then show ?thesis
-        apply (rule_tac x="(e * (b - a)) / 8 / norm (f' b)" in exI)
+        apply (rule_tac l="(e * (b - a)) / 8 / norm (f' b)" in that)
         using ab e
         apply (auto simp add: field_simps)
         done
     qed
-    then guess l .. note l = conjunctD2[OF this]
     show ?thesis
       apply (rule_tac x="min k l" in exI)
       apply safe
@@ -3818,7 +3792,7 @@
     note p = tagged_division_ofD[OF as(1)]
     have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
       using as by auto
-    note * = additive_tagged_division_1'[OF assms(1) as(1), symmetric]
+    note * = additive_tagged_division_1[OF assms(1) as(1), symmetric]
     have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
       by arith
     show ?case
@@ -3842,11 +3816,12 @@
         assume xk: "(x, k) \<in> p"
           "e * (Sup k -  Inf k) / 2 <
             norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))"
-        from p(4)[OF this(1)] guess u v by (elim exE) note k=this
+        obtain u v where k: "k = cbox u v"
+          using p(4) xk(1) by blast
         then have "u \<le> v" and uv: "{u, v} \<subseteq> cbox u v"
           using p(2)[OF xk(1)] by auto
-        note result = xk(2)[unfolded k box_real interval_bounds_real[OF this(1)] content_real[OF this(1)]]
-
+        then have result: "e * (v - u) / 2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
+          using xk(2)[unfolded k box_real interval_bounds_real content_real] by auto
         assume as': "x \<noteq> a" "x \<noteq> b"
         then have "x \<in> box a b"
           using p(2-3)[OF xk(1)] by (auto simp: mem_box)
@@ -3910,7 +3885,8 @@
           assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> {t. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
           then have xk: "(x, k) \<in> p" "content k = 0"
             by auto
-          from p(4)[OF xk(1)] guess u v by (elim exE) note uv=this
+          then obtain u v where uv: "k = cbox u v"
+            using p(4) by blast
           have "k \<noteq> {}"
             using p(2)[OF xk(1)] by auto
           then have *: "u = v"
@@ -3952,9 +3928,10 @@
             let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
             have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
             proof -
-              guess u v using p(4)[OF that] by (elim exE) note uv=this
-              have *: "u \<le> v"
-                using p(2)[OF that] unfolding uv by auto
+              obtain u v where uv: "k = cbox u v"
+                using \<open>(a, k) \<in> p\<close> p(4) by blast
+              then have *: "u \<le> v"
+                using p(2)[OF that] by auto
               have u: "u = a"
               proof (rule ccontr)
                 have "u \<in> cbox u v"
@@ -3975,7 +3952,8 @@
             qed
             have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
             proof -
-              guess u v using p(4)[OF that] by (elim exE) note uv=this
+              obtain u v where uv: "k = cbox u v"
+                using \<open>(b, k) \<in> p\<close> p(4) by blast
               have *: "u \<le> v"
                 using p(2)[OF that] unfolding uv by auto
               have u: "v = b"
@@ -6814,68 +6792,72 @@
     and "\<forall>x\<in>s. norm (f x) \<le> g x"
   shows "norm (integral s f) \<le> integral s g"
 proof -
-  have *: "\<And>x y. (\<forall>e::real. 0 < e \<longrightarrow> x < y + e) \<Longrightarrow> x \<le> y"
-    apply (rule ccontr)
-    apply (erule_tac x="x - y" in allE)
-    apply auto
-    done
   have norm: "norm ig < dia + e"
-    if "norm sg \<le> dsa"
-    and "\<bar>dsa - dia\<bar> < e / 2"
-    and "norm (sg - ig) < e / 2"
+    if "norm sg \<le> dsa" and "\<bar>dsa - dia\<bar> < e / 2" and "norm (sg - ig) < e / 2"
     for e dsa dia and sg ig :: 'a
     apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]])
     apply (subst real_sum_of_halves[of e,symmetric])
     unfolding add.assoc[symmetric]
     apply (rule add_le_less_mono)
-    defer
-    apply (subst norm_minus_commute)
-    apply (rule that(3))
+     defer
+     apply (subst norm_minus_commute)
+     apply (rule that(3))
     apply (rule order_trans[OF that(1)])
     using that(2)
     apply arith
     done
   have lem: "norm (integral(cbox a b) f) \<le> integral (cbox a b) g"
-    if "f integrable_on cbox a b"
-    and "g integrable_on cbox a b"
-    and "\<forall>x\<in>cbox a b. norm (f x) \<le> g x"
+    if f: "f integrable_on cbox a b"
+    and g: "g integrable_on cbox a b"
+    and nle: "\<And>x. x \<in> cbox a b \<Longrightarrow> norm (f x) \<le> g x"
     for f :: "'n \<Rightarrow> 'a" and g a b
-  proof (rule *[rule_format])
+  proof (rule eps_leI)
     fix e :: real
     assume "e > 0"
-    then have *: "e/2 > 0"
+    then have e: "e/2 > 0"
       by auto
-    from integrable_integral[OF that(1),unfolded has_integral[of f],rule_format,OF *]
-    guess d1 .. note d1 = conjunctD2[OF this,rule_format]
-    from integrable_integral[OF that(2),unfolded has_integral[of g],rule_format,OF *]
-    guess d2 .. note d2 = conjunctD2[OF this,rule_format]
-    note gauge_Int[OF d1(1) d2(1)]
-    from fine_division_exists[OF this, of a b] guess p . note p=this
+    with integrable_integral[OF f,unfolded has_integral[of f]]
+    obtain \<gamma> where \<gamma>: "gauge \<gamma>"
+              "\<And>p. p tagged_division_of cbox a b \<and> \<gamma> fine p 
+           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e / 2"
+      by meson 
+    moreover
+    from integrable_integral[OF g,unfolded has_integral[of g]] e
+    obtain \<delta> where \<delta>: "gauge \<delta>"
+              "\<And>p. p tagged_division_of cbox a b \<and> \<delta> fine p 
+           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g) < e / 2"
+      by meson
+    ultimately have "gauge (\<lambda>x. \<gamma> x \<inter> \<delta> x)"
+      using gauge_Int by blast
+    with fine_division_exists obtain p 
+      where p: "p tagged_division_of cbox a b" "(\<lambda>x. \<gamma> x \<inter> \<delta> x) fine p" 
+      by metis
+    have "\<gamma> fine p" "\<delta> fine p"
+      using fine_Int p(2) by blast+
     show "norm (integral (cbox a b) f) < integral (cbox a b) g + e"
-      apply (rule norm)
-      defer
-      apply (rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def])
-      defer
-      apply (rule d1(2)[OF conjI[OF p(1)]])
-      defer
-      apply (rule sum_norm_le)
-    proof safe
-      fix x k
-      assume "(x, k) \<in> p"
-      note as = tagged_division_ofD(2-4)[OF p(1) this]
-      from this(3) guess u v by (elim exE) note uv=this
-      show "norm (content k *\<^sub>R f x) \<le> content k *\<^sub>R g x"
-        unfolding uv norm_scaleR
-        unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def
-        apply (rule mult_left_mono)
-        using that(3) as
-        apply auto
-        done
-    qed (insert p[unfolded fine_Int], auto)
+    proof (rule norm)
+      have "norm (content K *\<^sub>R f x) \<le> content K *\<^sub>R g x" if  "(x, K) \<in> p" for x K
+      proof-
+        have K: "x \<in> K" "K \<subseteq> cbox a b"
+          using \<open>(x, K) \<in> p\<close> p(1) by blast+
+        obtain u v where  "K = cbox u v"
+          using \<open>(x, K) \<in> p\<close> p(1) by blast
+        moreover have "content K * norm (f x) \<le> content K * g x"
+          by (metis K subsetD dual_order.antisym measure_nonneg mult_zero_left nle not_le real_mult_le_cancel_iff2)
+        then show ?thesis
+          by simp
+      qed
+      then show "norm (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) \<le> (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
+        by (simp add: sum_norm_le split_def)
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e / 2"
+        using \<open>\<gamma> fine p\<close> \<gamma> p(1) by simp
+      show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g\<bar> < e / 2"
+        using \<open>\<delta> fine p\<close> \<delta> p(1) by simp
+    qed
   qed
 
   { presume "\<And>e. 0 < e \<Longrightarrow> norm (integral s f) < integral s g + e"
-    then show ?thesis by (rule *[rule_format]) auto }
+    then show ?thesis by (rule eps_leI) auto }
   fix e :: real
   assume "e > 0"
   then have e: "e/2 > 0"
@@ -6903,7 +6885,6 @@
     defer
     apply (rule w(2)[unfolded real_norm_def])
     apply (rule z(2))
-    apply safe
     apply (case_tac "x \<in> s")
     unfolding if_P
     apply (rule assms(3)[rule_format])
@@ -6911,6 +6892,7 @@
     done
 qed
 
+
 lemma integral_norm_bound_integral_component:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   fixes g :: "'n \<Rightarrow> 'b::euclidean_space"
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -1836,15 +1836,6 @@
 lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
   by (meson zero_less_one)
 
-lemma additive_tagged_division_1':
-  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
-  assumes "a \<le> b"
-    and "p tagged_division_of {a..b}"
-  shows "sum (\<lambda>(x,k). f (Sup k) - f(Inf k)) p = f b - f a"
-  using additive_tagged_division_1[OF _ assms(2), of f]
-  using assms(1)
-  by auto
-
 subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
 
 definition fine  (infixr "fine" 46)
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Equiv_Relations.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Equivalence Relations in Higher-Order Set Theory\<close>
 
 theory Equiv_Relations
-  imports Groups_Big Relation
+  imports Groups_Big
 begin
 
 subsection \<open>Equivalence relations -- set version\<close>
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Big sum and product over finite (non-empty) sets\<close>
 
 theory Groups_Big
-  imports Finite_Set Power
+  imports Power
 begin
 
 subsection \<open>Generic monoid operation over a set\<close>
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
 
 theory Lattices_Big
-imports Finite_Set Option
+  imports Option
 begin
 
 subsection \<open>Generic lattice operations over a set\<close>
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/List.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -4796,7 +4796,7 @@
 qed
 
 lemma card_lists_distinct_length_eq:
-  assumes "k < card A"
+  assumes "finite A" "k \<le> card A"
   shows "card {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A} = \<Prod>{card A - k + 1 .. card A}"
 using assms
 proof (induct k)
@@ -4808,25 +4808,32 @@
   let "?k_list" = "\<lambda>k xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A"
   have inj_Cons: "\<And>A. inj_on (\<lambda>(xs, n). n # xs) A"  by (rule inj_onI) auto
 
-  from Suc have "k < card A" by simp
-  moreover have "finite A" using assms by (simp add: card_ge_0_finite)
+  from Suc have "k \<le> card A" by simp
+  moreover note \<open>finite A\<close>
   moreover have "finite {xs. ?k_list k xs}"
     by (rule finite_subset) (use finite_lists_length_eq[OF \<open>finite A\<close>, of k] in auto)
   moreover have "\<And>i j. i \<noteq> j \<longrightarrow> {i} \<times> (A - set i) \<inter> {j} \<times> (A - set j) = {}"
     by auto
-  moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
+  moreover have "\<And>i. i \<in> {xs. ?k_list k xs} \<Longrightarrow> card (A - set i) = card A - k"
     by (simp add: card_Diff_subset distinct_card)
   moreover have "{xs. ?k_list (Suc k) xs} =
       (\<lambda>(xs, n). n#xs) ` \<Union>((\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs})"
     by (auto simp: length_Suc_conv)
-  moreover
-  have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
+  moreover have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
   then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
     by (subst prod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+
   ultimately show ?case
     by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps)
 qed
 
+lemma card_lists_distinct_length_eq':
+  assumes "k < card A"
+  shows "card {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> A} = \<Prod>{card A - k + 1 .. card A}"
+proof -
+  from \<open>k < card A\<close> have "finite A" and "k \<le> card A" using card_infinite by force+
+  from this show ?thesis by (rule card_lists_distinct_length_eq)
+qed
+
 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
 apply (rule notI)
 apply (drule finite_maxlen)
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Option.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Datatype option\<close>
 
 theory Option
-imports Lifting Finite_Set
+  imports Lifting
 begin
 
 datatype 'a option =
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Partial_Function.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -5,8 +5,8 @@
 section \<open>Partial Function Definitions\<close>
 
 theory Partial_Function
-imports Complete_Partial_Order Fun_Def_Base Option
-keywords "partial_function" :: thy_decl
+  imports Complete_Partial_Order Option
+  keywords "partial_function" :: thy_decl
 begin
 
 named_theorems partial_function_mono "monotonicity rules for partial function definitions"
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 07 15:10:37 2017 +0200
@@ -207,8 +207,6 @@
 
 (* E *)
 
-fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
-
 val e_smartN = "smart"
 val e_autoN = "auto"
 val e_fun_weightN = "fun_weight"
@@ -277,23 +275,19 @@
       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
     end
 
+val e_tff0 = TFF Monomorphic
+
 val e_config : atp_config =
-  {exec = fn full_proofs => (["E_HOME"],
-     if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"]
-     else ["eprover"]),
-   arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name =>
+  {exec = fn _ => (["E_HOME"], ["eprover"]),
+   arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
-       (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
-       "--tstp-in --tstp-out --silent " ^
+       "--auto-schedule --tstp-in --tstp-out --silent " ^
        e_selection_weight_arguments ctxt heuristic sel_weights ^
        e_term_order_info_arguments gen_weights gen_prec ord_info ^
        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
-       (if full_proofs orelse not (is_e_at_least_1_8 ()) then
-          " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2")
-        else
-          " --proof-object=1") ^
-       " " ^ file_name,
+       " --proof-object=1 " ^
+       file_name,
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
      tstp_proof_delims,
@@ -306,14 +300,14 @@
      let val heuristic = Config.get ctxt e_selection_heuristic in
        (* FUDGE *)
        if heuristic = e_smartN then
-         [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
-          (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
-          (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
-          (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
-          (0.15, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN)),
-          (0.25, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN))]
+         [(0.15, (((128, meshN), e_tff0, "mono_native", combsN, false), e_fun_weightN)),
+          (0.15, (((128, mashN), e_tff0, "mono_native", combsN, false), e_sym_offset_weightN)),
+          (0.15, (((91, mepoN), e_tff0, "mono_native", combsN, false), e_autoN)),
+          (0.15, (((1000, meshN), e_tff0, "poly_guards??", combsN, false), e_sym_offset_weightN)),
+          (0.15, (((256, mepoN), e_tff0, "mono_native", liftingN, false), e_fun_weightN)),
+          (0.25, (((64, mashN), e_tff0, "mono_native", combsN, false), e_fun_weightN))]
        else
-         [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
+         [(1.0, (((500, ""), e_tff0, "mono_native", combsN, false), heuristic))]
      end,
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
@@ -456,9 +450,8 @@
 val spass_extra_options =
   Attrib.setup_config_string @{binding atp_spass_extra_options} (K "")
 
-(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
 val spass_config : atp_config =
-  {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
+  {exec = K (["SPASS_HOME"], ["SPASS"]),
    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
        fn file_name => fn _ =>
        "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
@@ -710,7 +703,7 @@
     (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_e =
   remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
-    (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
+    (K (((750, ""), e_tff0, "mono_native", combsN, false), "") (* FUDGE *))
 val remote_iprover =
   remotify_atp iprover "iProver" ["0.99"]
     (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
@@ -724,7 +717,7 @@
   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
     (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["4.0", "3.0", "2.6"]
+  remotify_atp vampire "Vampire" ["4.2", "4.0"]
     (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/Tools/value_command.ML
--- a/src/HOL/Tools/value_command.ML	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/Tools/value_command.ML	Mon Aug 07 15:10:37 2017 +0200
@@ -17,9 +17,7 @@
 
 fun default_value ctxt t =
   if null (Term.add_frees t [])
-  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
-    SOME t' => t'
-  | NONE => Nbe.dynamic_value ctxt t
+  then Code_Evaluation.dynamic_value_strict ctxt t
   else Nbe.dynamic_value ctxt t;
 
 structure Evaluator = Theory_Data
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -38,7 +38,7 @@
 adhoc_overloading
   vars term_vars
 
-value "vars (Fun ''f'' [Var 0, Var 1])"
+value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
 
 fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
   "rule_vars (l, r) = vars l \<union> vars r"
@@ -46,7 +46,7 @@
 adhoc_overloading
   vars rule_vars
 
-value "vars (Var 1, Var 0)"
+value [nbe] "vars (Var 1, Var 0)"
 
 definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
   "trs_vars R = \<Union>(rule_vars ` R)"
@@ -54,7 +54,7 @@
 adhoc_overloading
   vars trs_vars
 
-value "vars {(Var 1, Var 0)}"
+value [nbe] "vars {(Var 1, Var 0)}"
 
 text \<open>Sometimes it is necessary to add explicit type constraints
 before a variant can be determined.\<close>
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/ex/Normalization_by_Evaluation.thy
--- a/src/HOL/ex/Normalization_by_Evaluation.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -68,20 +68,20 @@
 lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
   by normalization rule
 lemma "rev [a, b, c] = [c, b, a]" by normalization
-value "rev (a#b#cs) = rev cs @ [b, a]"
-value "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
-value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
-value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
+value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
+value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
+value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
+value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
 lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" 
   by normalization
-value "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
-value "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
+value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
+value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
 lemma "let x = y in [x, x] = [y, y]" by normalization
 lemma "Let y (%x. [x,x]) = [y, y]" by normalization
-value "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
+value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
 lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
-value "filter (%x. x) ([True,False,x]@xs)"
-value "filter Not ([True,False,x]@xs)"
+value [nbe] "filter (%x. x) ([True,False,x]@xs)"
+value [nbe] "filter Not ([True,False,x]@xs)"
 
 lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
 lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
@@ -106,7 +106,7 @@
 lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
 lemma "max (Suc 0) 0 = Suc 0" by normalization
 lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
-value "Suc 0 \<in> set ms"
+value [nbe] "Suc 0 \<in> set ms"
 
 (* non-left-linear patterns, equality by extensionality *)
 
@@ -115,13 +115,13 @@
 lemma "(f o g) x = f (g x)" by normalization
 lemma "(f o id) x = f x" by normalization
 lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
-value "(\<lambda>x. x)"
+value [nbe] "(\<lambda>x. x)"
 
 (* Church numerals: *)
 
-value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
 
 (* handling of type classes in connection with equality *)
 
diff -r 1f66c7d77002 -r a8b89392ecb6 src/HOL/ex/Transitive_Closure_Table_Ex.thy
--- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Mon Aug 07 15:10:37 2017 +0200
@@ -24,7 +24,7 @@
 values "{x. test\<^sup>*\<^sup>* A x}"
 values "{x. test\<^sup>*\<^sup>* x C}"
 
-value "test\<^sup>*\<^sup>* A C"
-value "test\<^sup>*\<^sup>* C A"
+value [nbe] "test\<^sup>*\<^sup>* A C"
+value [nbe] "test\<^sup>*\<^sup>* C A"
 
 end
diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Mon Aug 07 15:10:37 2017 +0200
@@ -115,6 +115,7 @@
       Options.isabelle_tool,
       Profiling_Report.isabelle_tool,
       Remote_DMG.isabelle_tool,
+      Server.isabelle_tool,
       Update_Cartouches.isabelle_tool,
       Update_Header.isabelle_tool,
       Update_Then.isabelle_tool,
diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/Pure/System/system_channel.scala	Mon Aug 07 15:10:37 2017 +0200
@@ -18,7 +18,7 @@
 
 class System_Channel private
 {
-  private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
+  private val server = new ServerSocket(0, 50, InetAddress.getByName("127.0.0.1"))
 
   val server_name: String = "127.0.0.1:" + server.getLocalPort
   override def toString: String = server_name
diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/Tools/server.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/server.scala	Mon Aug 07 15:10:37 2017 +0200
@@ -0,0 +1,180 @@
+/*  Title:      Pure/Tools/server.scala
+    Author:     Makarius
+
+Resident Isabelle servers.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
+  IOException}
+import java.net.{Socket, ServerSocket, InetAddress}
+
+
+object Server
+{
+  /* per-user servers */
+
+  object Data
+  {
+    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
+
+    val name = SQL.Column.string("name", primary_key = true)
+    val port = SQL.Column.int("port")
+    val password = SQL.Column.string("password")
+    val table = SQL.Table("isabelle_servers", List(name, port, password))
+
+    sealed case class Entry(name: String, port: Int, password: String)
+    {
+      def print: String =
+        "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")"
+
+      def active: Boolean =
+        try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true }
+        catch { case _: IOException => false }
+    }
+  }
+
+  def list(db: SQLite.Database): List[Data.Entry] =
+    if (db.tables.contains(Data.table.name)) {
+      db.using_statement(Data.table.select())(stmt =>
+        stmt.execute_query().iterator(res =>
+          Data.Entry(
+            res.string(Data.name),
+            res.int(Data.port),
+            res.string(Data.password))).toList.sortBy(_.name))
+    }
+    else Nil
+
+  def find(db: SQLite.Database, name: String): Option[Data.Entry] =
+    list(db).find(entry => entry.name == name && entry.active)
+
+  def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) =
+  {
+    using(SQLite.open_database(Data.database))(db =>
+      db.transaction {
+        find(db, name) match {
+          case Some(entry) => (entry, None)
+          case None =>
+            val server = new Server(port)
+            val entry = Data.Entry(name, server.port, server.password)
+
+            Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
+            db.create_table(Data.table)
+            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+            db.using_statement(Data.table.insert())(stmt =>
+            {
+              stmt.string(1) = entry.name
+              stmt.int(2) = entry.port
+              stmt.string(3) = entry.password
+              stmt.execute()
+            })
+
+            (entry, Some(server.thread))
+        }
+      })
+  }
+
+  def stop(name: String = ""): Boolean =
+  {
+    using(SQLite.open_database(Data.database))(db =>
+      db.transaction {
+        find(db, name) match {
+          case Some(entry) =>
+            // FIXME shutdown server
+            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+            true
+          case None =>
+            false
+        }
+      })
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
+    {
+      var operation_list = false
+      var name = ""
+      var port = 0
+
+      val getopts =
+        Getopts("""
+Usage: isabelle server [OPTIONS]
+
+  Options are:
+    -L           list servers
+    -n NAME      explicit server name
+    -p PORT      explicit server port
+
+  Manage resident Isabelle servers.
+""",
+          "L" -> (_ => operation_list = true),
+          "n:" -> (arg => name = arg),
+          "p:" -> (arg => port = Value.Int.parse(arg)))
+
+      val more_args = getopts(args)
+      if (more_args.nonEmpty) getopts.usage()
+
+      if (operation_list) {
+        for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
+          Console.println(entry.print)
+      }
+      else {
+        val (entry, thread) = start(name, port)
+        Console.println(entry.print)
+        thread.foreach(_.join)
+      }
+    })
+}
+
+class Server private(_port: Int)
+{
+  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
+  def port: Int = server_socket.getLocalPort
+  def close { server_socket.close }
+
+  val password: String = Library.UUID()
+
+  private def handle_connection(socket: Socket)
+  {
+    val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
+    val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
+
+    def println(s: String)
+    {
+      writer.write(s)
+      writer.newLine()
+      writer.flush()
+    }
+
+    reader.readLine() match {
+      case null =>
+      case bad if bad != password => println("BAD PASSWORD")
+      case _ =>
+        var finished = false
+        while (!finished) {
+          reader.readLine() match {
+            case null => println("FINISHED"); finished = true
+            case line => println("ECHO " + line)
+          }
+        }
+    }
+  }
+
+  lazy val thread: Thread =
+    Standard_Thread.fork("server") {
+      var finished = false
+      while (!finished) {
+        Exn.capture(server_socket.accept) match {
+          case Exn.Res(socket) =>
+            Standard_Thread.fork("server_connection")
+              { try { handle_connection(socket) } finally { socket.close } }
+          case Exn.Exn(_) => finished = true
+        }
+      }
+    }
+}
diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/build-jars
--- a/src/Pure/build-jars	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/Pure/build-jars	Mon Aug 07 15:10:37 2017 +0200
@@ -140,6 +140,7 @@
   Tools/main.scala
   Tools/print_operation.scala
   Tools/profiling_report.scala
+  Tools/server.scala
   Tools/simplifier_trace.scala
   Tools/spell_checker.scala
   Tools/task_statistics.scala
diff -r 1f66c7d77002 -r a8b89392ecb6 src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/Pure/library.scala	Mon Aug 07 15:10:37 2017 +0200
@@ -259,4 +259,9 @@
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
+
+
+  /* UUID */
+
+  def UUID(): String = java.util.UUID.randomUUID().toString
 }
diff -r 1f66c7d77002 -r a8b89392ecb6 src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/Tools/VSCode/src/grammar.scala	Mon Aug 07 15:10:37 2017 +0200
@@ -9,8 +9,6 @@
 
 import isabelle._
 
-import java.util.UUID
-
 
 object Grammar
 {
@@ -47,7 +45,7 @@
   "name": "Isabelle",
   "scopeName": "source.isabelle",
   "fileTypes": ["thy"],
-  "uuid": """ + JSON.Format(UUID.randomUUID().toString) + """,
+  "uuid": """ + JSON.Format(Library.UUID()) + """,
   "repository": {
     "comment": {
       "patterns": [
diff -r 1f66c7d77002 -r a8b89392ecb6 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 04 18:03:50 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 07 15:10:37 2017 +0200
@@ -12,7 +12,6 @@
 import javax.swing.JOptionPane
 
 import java.io.{File => JFile}
-import java.util.UUID
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
 import org.gjt.sp.jedit.textarea.JEditTextArea
@@ -398,7 +397,7 @@
 
   /* HTTP server */
 
-  val http_root: String = "/" + UUID.randomUUID().toString
+  val http_root: String = "/" + Library.UUID()
 
   val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))