--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Nov 01 18:24:10 2020 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Nov 05 19:09:02 2020 +0000
@@ -5799,7 +5799,8 @@
obtain u v where uv: "l = cbox u v"
using inp p'(4) by blast
have "content (cbox u v) = 0"
- unfolding content_eq_0_interior using that p(1) uv by auto
+ unfolding content_eq_0_interior using that p(1) uv
+ by (auto dest: tagged_partial_division_ofD)
then show ?thesis
using uv by blast
qed
@@ -5824,7 +5825,7 @@
shows "sum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e"
proof -
have "finite p"
- using tag by blast
+ using tag tagged_partial_division_ofD by blast
then show ?thesis
unfolding split_def
proof (rule sum_norm_allsubsets_bound)