src/HOL/Analysis/Great_Picard.thy

     with \<open>0 < r\<close> \<open>0 < m\<close> w w_inb show "deriv g w / g w = of_nat m / (w - z0) + deriv h w / h w"
       by (auto simp: geq divide_simps hnz)
   qed
   moreover
   have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. m / (z - z0) + deriv h z / h z) =
-        2 * of_real pi * ii * m + 0"
+        2 * of_real pi * \<i> * m + 0"
   proof (rule contour_integral_unique [OF has_contour_integral_add])
     show "((\<lambda>x. m / (x - z0)) has_contour_integral 2 * of_real pi * \<i> * m) (circlepath z0 (r/2))"
       by (force simp: \<open>0 < r\<close> intro: Cauchy_integral_circlepath_simple)
     show "((\<lambda>x. deriv h x / h x) has_contour_integral 0) (circlepath z0 (r/2))"
       apply (rule Cauchy_theorem_disc_simple [of _ z0 r])