# HG changeset patch # User haftmann # Date 1267645531 -3600 # Node ID 364cb98a3e4e40371114c44c4b72226486768034 # Parent 85aada96578b23a89dab9ff4716c15a143c0306d more uniform naming conventions diff -r 85aada96578b -r 364cb98a3e4e src/HOL/Map.thy --- a/src/HOL/Map.thy Wed Mar 03 17:21:47 2010 +0100 +++ b/src/HOL/Map.thy Wed Mar 03 20:45:31 2010 +0100 @@ -332,12 +332,12 @@ by (fastsimp simp: map_add_def dom_def inj_on_def split: option.splits) lemma map_upds_fold_map_upd: - "f(ks[\]vs) = foldl (\f (k, v). f(k\v)) f (zip ks vs)" + "m(ks[\]vs) = foldl (\m (k, v). m(k \ v)) m (zip ks vs)" unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length) fix ks :: "'a list" and vs :: "'b list" assume "length ks = length vs" - then show "foldl (\f (k, v). f(k\v)) f (zip ks vs) = f ++ map_of (rev (zip ks vs))" - by (induct arbitrary: f rule: list_induct2) simp_all + then show "foldl (\m (k, v). m(k\v)) m (zip ks vs) = m ++ map_of (rev (zip ks vs))" + by(induct arbitrary: m rule: list_induct2) simp_all qed lemma map_add_map_of_foldr: