--- a/src/HOL/Complex_Analysis/Contour_Integration.thy Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Thu Jun 03 10:47:20 2021 +0100
@@ -68,8 +68,8 @@
text\<open>Show that we can forget about the localized derivative.\<close>
lemma has_integral_localized_vector_derivative:
- "((\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow>
- ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}"
+ "((\<lambda>x. f (g x) * vector_derivative p (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow>
+ ((\<lambda>x. f (g x) * vector_derivative p (at x)) has_integral i) {a..b}"
proof -
have *: "{a..b} - {a,b} = interior {a..b}"
by (simp add: atLeastAtMost_diff_ends)
@@ -78,8 +78,8 @@
qed
lemma integrable_on_localized_vector_derivative:
- "(\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} \<longleftrightarrow>
- (\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}"
+ "(\<lambda>x. f (g x) * vector_derivative p (at x within {a..b})) integrable_on {a..b} \<longleftrightarrow>
+ (\<lambda>x. f (g x) * vector_derivative p (at x)) integrable_on {a..b}"
by (simp add: integrable_on_def has_integral_localized_vector_derivative)
lemma has_contour_integral: