src/HOL/Map.thy

--- a/src/HOL/Map.thy	Tue Jun 02 15:53:34 2009 +0200
+++ b/src/HOL/Map.thy	Tue Jun 02 16:23:43 2009 +0200
@@ -332,6 +332,9 @@
 lemma restrict_map_to_empty [simp]: "m|`{} = empty"
 by (simp add: restrict_map_def)
 
+lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
+by (auto simp add: restrict_map_def intro: ext)
+
 lemma restrict_map_empty [simp]: "empty|`D = empty"
 by (simp add: restrict_map_def)