src/HOL/Analysis/Complex_Transcendental.thy

     by simp
 next
   case False
   then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
     using Arg [of z]
-    by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
+    by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
   then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
     using cis_conv_exp cis_pi
     by (auto simp: exp_diff algebra_simps)
   then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg z) - pi)))"
     by simp

 lemma csqrt_exp_Ln:
   assumes "z \<noteq> 0"
     shows "csqrt z = exp(Ln(z) / 2)"
 proof -
   have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
-    by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
+    by (metis exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
   also have "... = z"
     using assms exp_Ln by blast
   finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
     by simp
   also have "... = exp (Ln z / 2)"