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