src/HOL/Map.thy
changeset 35553 a8c8008a2c9d
parent 35427 ad039d29e01c
parent 35552 364cb98a3e4e
child 35565 56b070cd7ab3
     1.1 --- a/src/HOL/Map.thy	Wed Mar 03 20:21:30 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Wed Mar 03 20:45:48 2010 +0100
     1.3 @@ -332,12 +332,12 @@
     1.4  by (fastsimp simp: map_add_def dom_def inj_on_def split: option.splits)
     1.5  
     1.6  lemma map_upds_fold_map_upd:
     1.7 -  "f(ks[\<mapsto>]vs) = foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs)"
     1.8 +  "m(ks[\<mapsto>]vs) = foldl (\<lambda>m (k, v). m(k \<mapsto> v)) m (zip ks vs)"
     1.9  unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length)
    1.10    fix ks :: "'a list" and vs :: "'b list"
    1.11    assume "length ks = length vs"
    1.12 -  then show "foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs) = f ++ map_of (rev (zip ks vs))"
    1.13 -    by (induct arbitrary: f rule: list_induct2) simp_all
    1.14 +  then show "foldl (\<lambda>m (k, v). m(k\<mapsto>v)) m (zip ks vs) = m ++ map_of (rev (zip ks vs))"
    1.15 +    by(induct arbitrary: m rule: list_induct2) simp_all
    1.16  qed
    1.17  
    1.18  lemma map_add_map_of_foldr: