src/HOL/Map.thy
changeset 31380 f25536c0bb80
parent 31080 21ffc770ebc0
child 32236 0203e1006f1b
     1.1 --- a/src/HOL/Map.thy	Tue Jun 02 15:53:34 2009 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Jun 02 16:23:43 2009 +0200
     1.3 @@ -332,6 +332,9 @@
     1.4  lemma restrict_map_to_empty [simp]: "m|`{} = empty"
     1.5  by (simp add: restrict_map_def)
     1.6  
     1.7 +lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
     1.8 +by (auto simp add: restrict_map_def intro: ext)
     1.9 +
    1.10  lemma restrict_map_empty [simp]: "empty|`D = empty"
    1.11  by (simp add: restrict_map_def)
    1.12