src/HOL/Map.thy
changeset 35619 b5f6481772f3
parent 35607 896f01fe825b
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Map.thy	Sat Mar 06 15:31:30 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Sat Mar 06 15:31:31 2010 +0100
     1.3 @@ -398,6 +398,10 @@
     1.4    "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
     1.5    by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
     1.6  
     1.7 +lemma restrict_complement_singleton_eq:
     1.8 +  "f |` (- {x}) = f(x := None)"
     1.9 +  by (simp add: restrict_map_def expand_fun_eq)
    1.10 +
    1.11  
    1.12  subsection {* @{term [source] map_upds} *}
    1.13  
    1.14 @@ -707,4 +711,3 @@
    1.15  qed
    1.16  
    1.17  end
    1.18 -