more uniform naming conventions
authorhaftmann
Wed Mar 03 20:45:31 2010 +0100 (2010-03-03)
changeset 35552364cb98a3e4e
parent 35551 85aada96578b
child 35553 a8c8008a2c9d
more uniform naming conventions
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Wed Mar 03 17:21:47 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Wed Mar 03 20:45:31 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: