src/HOL/Probability/Borel_Space.thy

   (is "_ = ?SIGMA")
 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
   fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
   then have "i \<in> Basis" by auto
   then have *: "{x::'a. x\<bullet>i \<le> a} = (\<Union>k::nat. {.. (\<Sum>n\<in>Basis. (if n = i then a else real k)*\<^sub>R n)})"
-  proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm)
+  proof (safe, simp_all add: eucl_le[where 'a='a] split: if_split_asm)
     fix x :: 'a
     from real_arch_simple[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"] guess k::nat ..
     then have "\<And>i. i \<in> Basis \<Longrightarrow> x\<bullet>i \<le> real k"
       by (subst (asm) Max_le_iff) auto
     then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia \<le> real k"

   fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
   then have i: "i \<in> Basis" by auto
   have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
   also have *: "{x::'a. a < x\<bullet>i} =
       (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
-  proof (safe, simp_all add: eucl_less_def split: split_if_asm)
+  proof (safe, simp_all add: eucl_less_def split: if_split_asm)
     fix x :: 'a
     from reals_Archimedean2[of "Max ((\<lambda>i. -x\<bullet>i)`Basis)"]
     guess k::nat .. note k = this
     { fix i :: 'a assume "i \<in> Basis"
       then have "-x\<bullet>i < real k"

 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
   fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
   then have i: "i \<in> Basis" by auto
   have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
   also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using \<open>i\<in> Basis\<close>
-  proof (safe, simp_all add: eucl_less_def split: split_if_asm)
+  proof (safe, simp_all add: eucl_less_def split: if_split_asm)
     fix x :: 'a
     from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"]
     guess k::nat .. note k = this
     { fix i :: 'a assume "i \<in> Basis"
       then have "x\<bullet>i < real k"

   let ?G = "\<lambda>y x. if g x = \<infinity> then H y \<infinity> else if g x = -\<infinity> then H y (-\<infinity>) else H y (ereal (real_of_ereal (g x)))"
   let ?F = "\<lambda>x. if f x = \<infinity> then ?G \<infinity> x else if f x = -\<infinity> then ?G (-\<infinity>) x else ?G (ereal (real_of_ereal (f x))) x"
   { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
   note * = this
   from assms show ?thesis
-    by (subst *) (simp del: space_borel split del: split_if)
+    by (subst *) (simp del: space_borel split del: if_split)
 qed
 
 lemma borel_measurable_ereal_iff:
   shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
 proof