changeset 14338 | a1add2de7601 |
parent 14328 | fd063037fdf5 |
child 14339 | ec575b7bde7a |
--- a/src/HOL/List.thy Mon Jan 05 00:46:06 2004 +0100 +++ b/src/HOL/List.thy Mon Jan 05 22:43:03 2004 +0100 @@ -488,8 +488,8 @@ by(induct ys, auto) lemma map_injective: - "!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys" -by (induct ys) auto + "!!xs. map f xs = map f ys ==> inj f ==> xs = ys" +by (induct ys) (auto dest!:injD) lemma inj_mapI: "inj f ==> inj (map f)" by (rules dest: map_injective injD intro: inj_onI)