# HG changeset patch
# User oheimb
# Date 1081792449 -7200
# Node ID e95ba267e3d523c7631841cde7c8254759801c2d
# Parent  43e436a4f2930a2ebe51da694f2921591acb87eb
added theorem chg_map_other

diff -r 43e436a4f293 -r e95ba267e3d5 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Apr 12 12:52:08 2004 +0200
+++ b/src/HOL/Map.thy	Mon Apr 12 19:54:09 2004 +0200
@@ -161,6 +161,9 @@
 lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
 by (unfold chg_map_def, auto)
 
+lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
+by (auto simp: chg_map_def split add: option.split)
+
 
 subsection {* @{term map_of} *}