# HG changeset patch
# User kleing
# Date 1073458332 -3600
# Node ID 6bc647f472b9c2bce588520b85bec0fc58ad188d
# Parent  6e564092d72d3a7483ff252eaa5193bb50e27ccc
map_idI

diff -r 6e564092d72d -r 6bc647f472b9 src/HOL/List.thy
--- 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} *}