src/HOL/Library/Landau_Symbols.thy

 proof -
   from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"
     by (rule asymp_equivD)
   from order_tendstoD(1)[OF this zero_less_one]
     show ?th1 ?th2 ?th3
-    by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+
+    by (eventually_elim; force simp: sgn_if field_split_simps split: if_splits)+
 qed
 
 lemma asymp_equiv_tendsto_transfer:
   assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"
   shows   "(g \<longlongrightarrow> c) F"

   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
   from landau_o.smallD[OF assms(2) zero_less_one]
     have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto
   have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"
     unfolding asymp_equiv_def using ev
-    by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)
+    by (intro tendsto_cong) (auto elim!: eventually_mono simp: field_split_simps)
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp
   also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)
   finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .
 qed
 

     by (intro tendsto_diff asymp_equivD tendsto_const)
   from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
   proof eventually_elim
     case (elim x)
     from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"
-      by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)
+      by (subst norm_mult [symmetric]) (auto split: if_splits simp add: algebra_simps)
     also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim
       by (auto split: if_splits simp: mult_right_mono)
     finally show ?case .
   qed
 qed