src/HOL/Analysis/Generalised_Binomial_Theorem.thy

   proof (rule has_field_derivative_zero_constant)
     fix z :: complex assume z': "z \<in> ball 0 K"
     hence z: "norm z < K" by simp
     with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique)
     from z K have "norm z < 1" by simp
-    hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff)
+    hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: Complex_eq complex_nonpos_Reals_iff)
     hence "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative
               f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z
       by (auto intro!: derivative_eq_intros)
     also from z have "a * f z = (1 + z) * f' z" by (rule deriv)
     finally show "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z within ball 0 K)"