src/HOL/Multivariate_Analysis/Derivative.thy

         qed
         hence "d' \<le> y"
           unfolding y_def
           by (rule cSup_upper) simp
         thus False using \<open>d > 0\<close> \<open>y < b\<close>
-          by (simp add: d'_def min_def split: split_if_asm)
+          by (simp add: d'_def min_def split: if_split_asm)
       qed
     } moreover {
       assume "a = y"
       with \<open>a < b\<close> have "y < b" by simp
       with \<open>a = y\<close> f_cont phi_cont \<open>e2 > 0\<close>

   moreover
   let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx x y) (x' - x)) \<le> norm (x' - x) * e"
   from fx[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
   have "\<forall>\<^sub>F x' in at x within X. ?le x'"
     by eventually_elim
-       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: split_if_asm)
+       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
   then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
     by (rule eventually_at_Pair_within_TimesI1)
        (simp add: blinfun.bilinear_simps)
   moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
     unfolding norm_eq_zero right_minus_eq