added theorem chg_map_other

--- 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} *}