src/HOL/Probability/Radon_Nikodym.thy

       by (auto intro!: someI2[of _ _ "\<lambda>A. A \<in> sets M"] simp: not_less) }
   note A'_in_sets = this
   { fix n have "A n \<in> sets M"
     proof (induct n)
       case (Suc n) thus "A (Suc n) \<in> sets M"
-        using A'_in_sets[of "A n"] by (auto split: split_if_asm)
+        using A'_in_sets[of "A n"] by (auto split: if_split_asm)
     qed (simp add: A_def) }
   note A_in_sets = this
   hence "range A \<subseteq> sets M" by auto
   { fix n B
     assume Ex: "\<exists>B. B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> -e"

   moreover have "AE x in M. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
     ?f (space M) x = ?f' (space M) x"
     by (auto simp: indicator_def Q0)
   ultimately have "AE x in M. ?f (space M) x = ?f' (space M) x"
     unfolding AE_all_countable[symmetric]
-    by eventually_elim (auto intro!: AE_I2 split: split_if_asm simp: indicator_def)
+    by eventually_elim (auto intro!: AE_I2 split: if_split_asm simp: indicator_def)
   then show "AE x in M. f x = f' x" by auto
 qed
 
 lemma (in sigma_finite_measure) density_unique:
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"