# HG changeset patch
# User nipkow
# Date 1052901232 -7200
# Node ID c031a330a03f81955f92cbdff3e6e258d7117865
# Parent  d9b155757dc892f45907bc1f5f09d08402faaf05
*** empty log message ***

diff -r d9b155757dc8 -r c031a330a03f src/HOL/Map.thy
--- 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)