map_idI

--- a/src/HOL/List.thy	Tue Jan 06 10:50:36 2004 +0100
+++ b/src/HOL/List.thy	Wed Jan 07 07:52:12 2004 +0100
@@ -507,6 +507,8 @@
 lemma inj_map[iff]: "inj (map f) = inj f"
 by (blast dest: inj_mapD intro: inj_mapI)
 
+lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
+by (induct xs, auto)
 
 subsection {* @{text rev} *}