diff -r c85efa2be619 -r 934e0044e94b src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Nov 04 17:06:18 2019 +0000
@@ -2269,7 +2269,7 @@
   case False
   show ?thesis
     unfolding powr_def
-  proof (rule DERIV_transform_at)
+  proof (rule has_field_derivative_transform_within)
     show "((\<lambda>z. exp (s * Ln z)) has_field_derivative s * (if z = 0 then 0 else exp ((s - 1) * Ln z)))
            (at z)"
       apply (intro derivative_eq_intros | simp add: assms)+
@@ -2761,7 +2761,7 @@
   with z have "((\<lambda>z. exp (Ln z / 2)) has_field_derivative inverse (2 * csqrt z)) (at z)"
     by (force intro: derivative_eq_intros * simp add: assms)
   then show ?thesis
-  proof (rule DERIV_transform_at)
+  proof (rule has_field_derivative_transform_within)
     show "\<And>x. dist x z < cmod z \<Longrightarrow> exp (Ln x / 2) = csqrt x"
       by (metis csqrt_exp_Ln dist_0_norm less_irrefl)
   qed (use z in auto)