src/HOL/Map.thy
changeset 61032 b57df8eecad6
parent 60841 144523e0678e
child 61069 aefe89038dd2
     1.1 --- a/src/HOL/Map.thy	Thu Aug 27 13:07:45 2015 +0200
     1.2 +++ b/src/HOL/Map.thy	Thu Aug 27 21:19:48 2015 +0200
     1.3 @@ -227,14 +227,14 @@
     1.4  
     1.5  lemma map_of_mapk_SomeI:
     1.6    "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>
     1.7 -   map_of (map (split (\<lambda>k. Pair (f k))) t) (f k) = Some x"
     1.8 +   map_of (map (case_prod (\<lambda>k. Pair (f k))) t) (f k) = Some x"
     1.9  by (induct t) (auto simp: inj_eq)
    1.10  
    1.11  lemma weak_map_of_SomeI: "(k, x) \<in> set l \<Longrightarrow> \<exists>x. map_of l k = Some x"
    1.12  by (induct l) auto
    1.13  
    1.14  lemma map_of_filter_in:
    1.15 -  "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
    1.16 +  "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (case_prod P) xs) k = Some z"
    1.17  by (induct xs) auto
    1.18  
    1.19  lemma map_of_map: