| changeset 14343 | 6bc647f472b9 |
| parent 14339 | ec575b7bde7a |
| child 14388 | 04f04408b99b |
--- 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} *}