*** empty log message ***
authornipkow
Wed May 14 10:33:52 2003 +0200 (2003-05-14)
changeset 14026c031a330a03f
parent 14025 d9b155757dc8
child 14027 68d247b7b14b
*** empty log message ***
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Wed May 14 10:22:09 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed May 14 10:33:52 2003 +0200
     1.3 @@ -201,6 +201,11 @@
     1.4  apply(simp add: map_add_def split:option.split)
     1.5  done
     1.6  
     1.7 +lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
     1.8 +apply(rule ext)
     1.9 +apply(fastsimp simp:map_add_def split:option.split)
    1.10 +done
    1.11 +
    1.12  lemma map_add_Some_iff: 
    1.13   "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
    1.14  apply (unfold map_add_def)