--- a/src/HOL/Complex.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Complex.thy Tue Oct 08 10:26:40 2019 +0000
@@ -480,7 +480,7 @@
((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def
- tendsto_complex_iff field_simps bounded_linear_scaleR_left bounded_linear_mult_right)
+ tendsto_complex_iff algebra_simps bounded_linear_scaleR_left bounded_linear_mult_right)
lemma has_field_derivative_Re[derivative_intros]:
"(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Re (f x)) has_field_derivative (Re D)) F"