src/HOL/Map.thy
changeset 62390 842917225d56
parent 61955 e96292f32c3c
child 63648 f9f3006a5579
     1.1 --- a/src/HOL/Map.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Map.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -358,10 +358,10 @@
     1.4  by (simp add: restrict_map_def)
     1.5  
     1.6  lemma ran_restrictD: "y \<in> ran (m|`A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
     1.7 -by (auto simp: restrict_map_def ran_def split: split_if_asm)
     1.8 +by (auto simp: restrict_map_def ran_def split: if_split_asm)
     1.9  
    1.10  lemma dom_restrict [simp]: "dom (m|`A) = dom m \<inter> A"
    1.11 -by (auto simp: restrict_map_def dom_def split: split_if_asm)
    1.12 +by (auto simp: restrict_map_def dom_def split: if_split_asm)
    1.13  
    1.14  lemma restrict_upd_same [simp]: "m(x\<mapsto>y)|`(-{x}) = m|`(-{x})"
    1.15  by (rule ext) (auto simp: restrict_map_def)
    1.16 @@ -429,7 +429,7 @@
    1.17  apply (induct xs arbitrary: x y ys f)
    1.18   apply simp
    1.19  apply (case_tac ys)
    1.20 - apply (auto split: split_if simp: fun_upd_twist)
    1.21 + apply (auto split: if_split simp: fun_upd_twist)
    1.22  done
    1.23  
    1.24  lemma map_upds_twist [simp]:
    1.25 @@ -691,7 +691,7 @@
    1.26  lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
    1.27  proof(rule iffI)
    1.28    assume "\<exists>v. f = [x \<mapsto> v]"
    1.29 -  thus "dom f = {x}" by(auto split: split_if_asm)
    1.30 +  thus "dom f = {x}" by(auto split: if_split_asm)
    1.31  next
    1.32    assume "dom f = {x}"
    1.33    then obtain v where "f x = Some v" by auto