# HG changeset patch
# User nipkow
# Date 1073340632 -3600
# Node ID ec575b7bde7a08b60b5f29f2f98d148c90bdf94a
# Parent  a1add2de7601b24c3f4f8eb9e5807fb135d1cb4c
*** empty log message ***

diff -r a1add2de7601 -r ec575b7bde7a src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jan 05 22:43:03 2004 +0100
+++ b/src/HOL/List.thy	Mon Jan 05 23:10:32 2004 +0100
@@ -491,6 +491,9 @@
  "!!xs. map f xs = map f ys ==> inj f ==> xs = ys"
 by (induct ys) (auto dest!:injD)
 
+lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
+by(blast dest:map_injective)
+
 lemma inj_mapI: "inj f ==> inj (map f)"
 by (rules dest: map_injective injD intro: inj_onI)
 
@@ -501,7 +504,7 @@
 apply blast
 done
 
-lemma inj_map: "inj (map f) = inj f"
+lemma inj_map[iff]: "inj (map f) = inj f"
 by (blast dest: inj_mapD intro: inj_mapI)