src/HOL/Limits.thy

   unfolding filterlim_at_top_gt[where c=0]
 proof safe
   fix Z :: real assume "0 < Z"
   from f \<open>0 < c\<close> have "eventually (\<lambda>x. c / 2 < f x) F"
     by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_mono
-             simp: dist_real_def abs_real_def split: split_if_asm)
+             simp: dist_real_def abs_real_def split: if_split_asm)
   moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F"
     unfolding filterlim_at_top by auto
   ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F"
   proof eventually_elim
     fix x assume "c / 2 < f x" "Z / c * 2 \<le> g x"