src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
 changeset 69313 b021008c5397 parent 69064 5840724b1d71 child 69508 2a4c8a2a3f8e
```     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Nov 18 09:51:41 2018 +0100
1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Nov 18 18:07:51 2018 +0000
1.3 @@ -5635,15 +5635,15 @@
1.4          using qq by auto
1.5        show "\<And>i1 i2. \<lbrakk>i1 \<in> r; i2 \<in> r; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior i1 \<inter> interior i2 = {}"
1.6          by (simp add: q'(5) r_def)
1.7 -      show "interior (UNION p snd) \<inter> interior (\<Union>r) = {}"
1.8 +      show "interior (\<Union>(snd ` p)) \<inter> interior (\<Union>r) = {}"
1.9        proof (rule Int_interior_Union_intervals [OF \<open>finite r\<close>])
1.10 -        show "open (interior (UNION p snd))"
1.11 +        show "open (interior (\<Union>(snd ` p)))"
1.12            by blast
1.13          show "\<And>T. T \<in> r \<Longrightarrow> \<exists>a b. T = cbox a b"
1.14            by (simp add: q'(4) r_def)
1.15          have "finite (snd ` p)"
1.17 -        then show "\<And>T. T \<in> r \<Longrightarrow> interior (UNION p snd) \<inter> interior T = {}"
1.18 +        then show "\<And>T. T \<in> r \<Longrightarrow> interior (\<Union>(snd ` p)) \<inter> interior T = {}"
1.19            apply (subst Int_commute)
1.20            apply (rule Int_interior_Union_intervals)
1.21            using r_def q'(5) q(1) apply auto
1.22 @@ -5672,7 +5672,7 @@
1.23        then show "content L *\<^sub>R f x = 0"
1.24          unfolding uv content_eq_0_interior[symmetric] by auto
1.25      qed
1.26 -    show "finite (UNION r qq)"
1.27 +    show "finite (\<Union>(qq ` r))"
1.28        by (meson finite_UN qq \<open>finite r\<close> tagged_division_of_finite)
1.29    qed
1.30    moreover have "content M *\<^sub>R f x = 0"
```