src/HOL/Map.thy
changeset 14537 e95ba267e3d5
parent 14376 9fe787a90a48
child 14739 86c6f272ef79
     1.1 --- a/src/HOL/Map.thy	Mon Apr 12 12:52:08 2004 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Apr 12 19:54:09 2004 +0200
     1.3 @@ -161,6 +161,9 @@
     1.4  lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
     1.5  by (unfold chg_map_def, auto)
     1.6  
     1.7 +lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
     1.8 +by (auto simp: chg_map_def split add: option.split)
     1.9 +
    1.10  
    1.11  subsection {* @{term map_of} *}
    1.12