src/HOL/Analysis/Starlike.thy

           show "dist (x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a)) x < e"
             using \<open>0 < e\<close> by (auto simp: dist_norm min_def)
           show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<in> interior S"
             apply (clarsimp simp add: min_def a)
             apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
-            using \<open>0 < e\<close> False apply (auto simp: divide_simps)
+            using \<open>0 < e\<close> False apply (auto simp: field_split_simps)
             done
         qed
       qed
     qed
   qed

           show ?thesis
             using e [OF ain] nonrel dle by force
       qed
     qed
     then show False
-      using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] divide_simps)
+      using \<open>0 < e\<close> \<open>l \<noteq> 0\<close> by (simp add: d_def [symmetric] field_simps)
   qed
   moreover have "a + d *\<^sub>R l \<in> closure S"
   proof (clarsimp simp: closure_approachable)
     fix \<eta>::real assume "0 < \<eta>"
     have 1: "a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l \<in> S"
       apply (rule subsetD [OF rel_interior_subset inint])
       using \<open>l \<noteq> 0\<close> \<open>0 < d\<close> \<open>0 < \<eta>\<close> by auto
     have "norm l * min d (\<eta> / (norm l * 2)) \<le> norm l * (\<eta> / (norm l * 2))"
       by (metis min_def mult_left_mono norm_ge_zero order_refl)
     also have "... < \<eta>"
-      using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: divide_simps)
+      using \<open>l \<noteq> 0\<close> \<open>0 < \<eta>\<close> by (simp add: field_simps)
     finally have 2: "norm l * min d (\<eta> / (norm l * 2)) < \<eta>" .
     show "\<exists>y\<in>S. dist y (a + d *\<^sub>R l) < \<eta>"
       apply (rule_tac x="a + (d - min d (\<eta> / 2 / norm l)) *\<^sub>R l" in bexI)
       using 1 2 \<open>0 < d\<close> \<open>0 < \<eta>\<close> apply (auto simp: algebra_simps)
       done

       using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast
     moreover have "x + d *\<^sub>R (y - x) \<in> open_segment x y" if "d < 1"
       using xy
       apply (auto simp: in_segment)
       apply (rule_tac x="d" in exI)
-      using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps)
+      using \<open>0 < d\<close> that apply (auto simp: algebra_simps)
       done
     ultimately have "1 \<le> d"
       using df rel_frontier_def by fastforce
     moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x"
       by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
     ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y - x))"
       apply (auto simp: in_segment)
       apply (rule_tac x="1/d" in exI)
-      apply (auto simp: divide_simps algebra_simps)
+      apply (auto simp: algebra_simps)
       done
   next
     show "open_segment x (x + d *\<^sub>R (y - x)) \<subseteq> rel_interior S"
       apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x])
       using df rel_frontier_def by auto

       moreover have "a /\<^sub>R (norm a) \<in> span S"
         by (simp add: \<open>a \<in> S\<close> span_scale span_base)
       ultimately have ass: "a /\<^sub>R (norm a) \<in> span S \<inter> sphere 0 1"
         by simp
       have aa: "a /\<^sub>R (norm a) \<in> (\<Inter>c\<in>C. {x. 0 \<le> c \<bullet> x})"
-        apply (clarsimp simp add: divide_simps)
+        apply (clarsimp simp add: field_split_simps)
         using ab \<open>0 < b\<close>
         by (metis hull_inc inner_commute less_eq_real_def less_trans)
       show ?thesis
         apply (simp add: C k_def)
         using ass aa Int_iff empty_iff by blast

       have "closure (\<Union>x\<in>- S. \<Union>y\<in>ball 0 (1 / (2 + real n)). {x + y})
             \<subseteq> (\<Union>x \<in> -S. \<Union>e \<in> cball 0 (1 / (2 + real n)). {x + e})"
         by (intro closure_minimal UN_mono ball_subset_cball order_refl cl)
       also have "... \<subseteq> (\<Union>x \<in> -S. \<Union>y\<in>ball 0 (1 / (1 + real n)). {x + y})"
         apply (intro UN_mono order_refl)
-        apply (simp add: cball_subset_ball_iff divide_simps)
+        apply (simp add: cball_subset_ball_iff field_split_simps)
         done
       finally show "closure (\<Union>x\<in>- S. \<Union>y\<in>ball 0 (1 / (2 + real n)). {x + y})
                     \<subseteq> (\<Union>x \<in> -S. \<Union>y\<in>ball 0 (1 / (1 + real n)). {x + y})" .
     qed
     have "S \<subseteq> \<Union> (range ?C)"

         using reals_Archimedean2
         by (metis divide_less_0_iff less_eq_real_def neq0_conv not_le of_nat_0 of_nat_1 of_nat_less_0_iff)
       obtain N2 where N2: "norm(x - a) \<le> real N2"
         by (meson real_arch_simple)
       have N12: "inverse((N1 + N2) + 1) \<le> inverse(N1)"
-        using \<open>N1 > 0\<close> by (auto simp: divide_simps)
+        using \<open>N1 > 0\<close> by (auto simp: field_split_simps)
       have "x \<noteq> y + z" if "y \<notin> S" "norm z < 1 / (1 + (real N1 + real N2))" for y z
       proof -
         have "e * real N1 < e * (1 + (real N1 + real N2))"
           by (simp add: \<open>0 < e\<close>)
         then have "1 / (1 + (real N1 + real N2)) < e"