src/HOL/Library/AssocList.thy
changeset 37591 d3daea901123
parent 37458 4a76497f2eaa
child 37608 165cd386288d
     1.1 --- a/src/HOL/Library/AssocList.thy	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Mon Jun 28 15:03:07 2010 +0200
     1.3 @@ -427,8 +427,7 @@
     1.4  
     1.5  lemma merge_updates:
     1.6    "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
     1.7 -  by (simp add: merge_def updates_def split_prod_case
     1.8 -    foldr_fold_rev zip_rev zip_map_fst_snd)
     1.9 +  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
    1.10  
    1.11  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
    1.12    by (induct ys arbitrary: xs) (auto simp add: dom_update)
    1.13 @@ -449,7 +448,7 @@
    1.14      More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
    1.15      by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
    1.16    then show ?thesis
    1.17 -    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq)
    1.18 +    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq)
    1.19  qed
    1.20  
    1.21  corollary merge_conv: