changeset 14026 | c031a330a03f |
parent 14025 | d9b155757dc8 |
child 14027 | 68d247b7b14b |
--- a/src/HOL/Map.thy Wed May 14 10:22:09 2003 +0200 +++ b/src/HOL/Map.thy Wed May 14 10:33:52 2003 +0200 @@ -201,6 +201,11 @@ apply(simp add: map_add_def split:option.split) done +lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1" +apply(rule ext) +apply(fastsimp simp:map_add_def split:option.split) +done + lemma map_add_Some_iff: "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)" apply (unfold map_add_def)