src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

   and f0: "Df 0 = f"
   and Df: "\<And>m t. m < p \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
     (Df m has_vector_derivative Df (Suc m) t) (at t within {a..b})"
   and ivl: "a \<le> b"
   defines "i \<equiv> \<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x"
-  shows taylor_has_integral:
+  shows Taylor_has_integral:
     "(i has_integral f b - (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
-  and taylor_integral:
+  and Taylor_integral:
     "f b = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
-  and taylor_integrable:
+  and Taylor_integrable:
     "i integrable_on {a..b}"
 proof goal_cases
   case 1
   interpret bounded_bilinear "scaleR::real\<Rightarrow>'a\<Rightarrow>'a"
     by (rule bounded_bilinear_scaleR)