src/HOL/Analysis/Riemann_Mapping.thy

               by (rule has_contour_integral_diff [OF z con])
             show "\<And>w. w \<in> closed_segment x y \<Longrightarrow> norm (f w - f x) \<le> e/2"
               by (metis d1 dist_norm less_le_trans not_less not_less_iff_gr_or_eq segment_bound1 that(4))
           qed (use \<open>e > 0\<close> in auto)
           with \<open>e > 0\<close> have "inverse (norm (y - x)) * norm (z - f x * (y - x)) \<le> e/2"
-            by (simp add: divide_simps)
+            by (simp add: field_split_simps)
           also have "... < e"
             using \<open>e > 0\<close> by simp
           finally show ?thesis
             by (simp add: contour_integral_unique [OF z])
         qed

       using norm_triangle_ineq4 [of x y] by simp
     have "norm ((r/3) / (g z + g a) - (r/3) / (g a + g a)) < 1" if "z \<in> S" for z
       apply (rule 3)
       unfolding norm_divide
       using \<open>r > 0\<close> g_not_r [OF \<open>z \<in> S\<close>] g_not_r [OF \<open>a \<in> S\<close>]
-      by (simp_all add: divide_simps dist_commute dist_norm)
+      by (simp_all add: field_split_simps dist_commute dist_norm)
   then show "?f ` S \<subseteq> ball 0 1"
     by auto
     show "inj_on ?f S"
       using \<open>r > 0\<close> eqg apply (clarsimp simp: inj_on_def)
       by (metis diff_add_cancel)

       proof (clarify, clarsimp simp: X_def fim [symmetric])
         fix x assume x [rule_format]: "\<forall>n. f x \<in> closure (f ` A n)" and "cmod x < 1"
         then obtain n where n: "1 / (1 - norm x) < of_nat n"
           using reals_Archimedean2 by blast
         with \<open>cmod x < 1\<close> gr0I have XX: "1 / of_nat n < 1 - norm x" and "n > 0"
-          by (fastforce simp: divide_simps algebra_simps)+
+          by (fastforce simp: field_split_simps algebra_simps)+
         have "f x \<in> f ` (D n)"
-          using n \<open>cmod x < 1\<close> by (auto simp: divide_simps algebra_simps D_def)
+          using n \<open>cmod x < 1\<close> by (auto simp: field_split_simps algebra_simps D_def)
         moreover have " f ` D n \<inter> closure (f ` A n) = {}"
         proof -
           have op_fDn: "open(f ` (D n))"
           proof (rule invariance_of_domain)
             show "continuous_on (D n) f"