src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 64911 f0e07600de47
parent 64773 223b2ebdda79
child 65036 ab7e11730ad8
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4    fixes a :: "'a::euclidean_space"
     1.5    assumes "k \<in> Basis"
     1.6    shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
     1.7 -  -- \<open>Prove using measure theory\<close>
     1.8 +  \<comment> \<open>Prove using measure theory\<close>
     1.9  proof cases
    1.10    note simps = interval_split[OF assms] content_cbox_cases
    1.11    have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"