*** empty log message ***
authornipkow
Mon Jan 05 22:43:03 2004 +0100 (2004-01-05)
changeset 14338a1add2de7601
parent 14337 e13731554e50
child 14339 ec575b7bde7a
*** empty log message ***
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Mon Jan 05 00:46:06 2004 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Jan 05 22:43:03 2004 +0100
     1.3 @@ -488,8 +488,8 @@
     1.4  by(induct ys, auto)
     1.5  
     1.6  lemma map_injective:
     1.7 - "!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys"
     1.8 -by (induct ys) auto
     1.9 + "!!xs. map f xs = map f ys ==> inj f ==> xs = ys"
    1.10 +by (induct ys) (auto dest!:injD)
    1.11  
    1.12  lemma inj_mapI: "inj f ==> inj (map f)"
    1.13  by (rules dest: map_injective injD intro: inj_onI)