# 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 \ b \ chg_map f a m b = m b" +by (auto simp: chg_map_def split add: option.split) + subsection {* @{term map_of} *}