--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Apr 14 09:23:00 2018 +0100
@@ -5258,7 +5258,7 @@
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "f integrable_on S" "f integrable_on T" "negligible (S \<inter> T)"
shows "integral (S \<union> T) f = integral S f + integral T f"
- using has_integral_Un by (simp add: has_integral_Un assms integrable_integral integral_unique)
+ by (simp add: has_integral_Un assms integrable_integral integral_unique)
lemma integrable_Un:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"