# HG changeset patch
# User haftmann
# Date 1243970027 -7200
# Node ID ac7abb2e5944be27e940beea03a0a39b1df9909d
# Parent  5c563b9688327a423010f4fd23270a6966752dca
moved restrict_map_insert to theory Map

diff -r 5c563b968832 -r ac7abb2e5944 src/HOL/Library/Fin_Fun.thy
--- a/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 18:26:12 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 21:13:47 2009 +0200
@@ -17,10 +17,6 @@
   For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
 *}
 
-(*FIXME move to Map.thy*)
-lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
-  by (auto simp add: restrict_map_def intro: ext)
-
 
 subsection {* The @{text "map_default"} operation *}