src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

     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 = {}"
       by metis
     have "e/2 > 0"
       using e by auto
-    with henstock_lemma[OF f] 
+    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. \<gamma> x \<inter> ball x (k x)"

             norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e/2"
           unfolding has_integral_integral has_integral by meson
         obtain d2 where "gauge d2" 
           and d2: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); d2 fine p\<rbrakk> \<Longrightarrow>
             (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
-          by (blast intro: henstock_lemma [OF f(1) \<open>e/2>0\<close>])
+          by (blast intro: Henstock_lemma [OF f(1) \<open>e/2>0\<close>])
         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 \<open>gauge d1\<close> \<open>gauge d2\<close>], of a b])
             (auto simp add: fine_Int)
         have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> ?S; \<bar>sf - si\<bar> < e/2;