src/HOL/Word/Word.thy

 (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
 ML \<open>
 fun uint_arith_simpset ctxt = 
   ctxt addsimps @{thms uint_arith_simps}
      delsimps @{thms word_uint.Rep_inject}
-     |> fold Splitter.add_split @{thms split_if_asm}
+     |> fold Splitter.add_split @{thms if_split_asm}
      |> fold Simplifier.add_cong @{thms power_False_cong}
 
 fun uint_arith_tacs ctxt = 
   let
     fun arith_tac' n t =

   "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
     0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
   using [[simproc del: linordered_ring_less_cancel_factor]]
   apply (unfold udvd_def)
   apply clarify
-  apply (simp add: uint_arith_simps split: split_if_asm)
+  apply (simp add: uint_arith_simps split: if_split_asm)
    prefer 2 
    apply (insert uint_range' [of s])[1]
    apply arith
   apply (drule add.commute [THEN xtr1])
   apply (simp add: diff_less_eq [symmetric])

    try to solve via arith *)
 ML \<open>
 fun unat_arith_simpset ctxt = 
   ctxt addsimps @{thms unat_arith_simps}
      delsimps @{thms word_unat.Rep_inject}
-     |> fold Splitter.add_split @{thms split_if_asm}
+     |> fold Splitter.add_split @{thms if_split_asm}
      |> fold Simplifier.add_cong @{thms power_False_cong}
 
 fun unat_arith_tacs ctxt =   
   let
     fun arith_tac' n t =

   note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
   note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
 
   show ?thesis
   apply (unfold word_rot_defs)
-  apply (simp only: split: split_if)
+  apply (simp only: split: if_split)
   apply (safe intro!: abl_cong)
   apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse'] 
                     to_bl_rotl
                     to_bl_rotr [THEN word_bl.Rep_inverse']
                     to_bl_rotr)