src/HOL/Map.thy

 lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3"
 apply(rule ext)
 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)
 apply (simp (no_asm) split add: option.split)
 done

 
 lemma dom_overwrite[simp]:
  "dom(f(g|A)) = (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
 by(auto simp add: dom_def overwrite_def)
 
+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
+
 subsection {* ran *}
 
 lemma ran_empty[simp]: "ran empty = {}"
 apply (unfold ran_def)
 apply (simp (no_asm))