src/HOL/Library/AList.thy

 
 lemma update_eqD: "update k v al = update k v' al' \<Longrightarrow> v = v'"
 proof (induct al arbitrary: al')
   case Nil
   then show ?case
-    by (cases al') (auto split: split_if_asm)
+    by (cases al') (auto split: if_split_asm)
 next
   case Cons
   then show ?case
-    by (cases al') (auto split: split_if_asm)
+    by (cases al') (auto split: if_split_asm)
 qed
 
 lemma update_last [simp]: "update k v (update k v' al) = update k v al"
   by (induct al) auto
 

 lemma map_of_delete_aux:
   "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
 by(simp add: map_of_delete_aux')
 
 lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
-by(cases ts)(auto split: split_if_asm)
+by(cases ts)(auto split: if_split_asm)
 
 
 subsection \<open>\<open>restrict\<close>\<close>
 
 qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"

   by (relation "measure (length \<circ> fst)") (simp_all add: less_Suc_eq_le length_delete_le)
 
 lemma compose_first_None [simp]:
   assumes "map_of xs k = None"
   shows "map_of (compose xs ys) k = None"
-  using assms by (induct xs ys rule: compose.induct) (auto split: option.splits split_if_asm)
+  using assms by (induct xs ys rule: compose.induct) (auto split: option.splits if_split_asm)
 
 lemma compose_conv: "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
 proof (induct xs ys rule: compose.induct)
   case 1
   then show ?case by simp