src/HOL/List.thy
changeset 13585 db4005b40cc6
parent 13508 890d736b93a5
child 13601 fd3e3d6b37b2
     1.1 --- a/src/HOL/List.thy	Thu Sep 26 10:43:43 2002 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Sep 26 10:51:29 2002 +0200
     1.3 @@ -451,7 +451,7 @@
     1.4  by (induct ys) (auto simp add: map_eq_Cons)
     1.5  
     1.6  lemma inj_mapI: "inj f ==> inj (map f)"
     1.7 -by (rules dest: map_injective injD intro: injI)
     1.8 +by (rules dest: map_injective injD intro: inj_onI)
     1.9  
    1.10  lemma inj_mapD: "inj (map f) ==> inj f"
    1.11  apply (unfold inj_on_def)
    1.12 @@ -1241,7 +1241,7 @@
    1.13  apply(rule wf_subset)
    1.14   prefer 2 apply (rule Int_lower1)
    1.15  apply(rule wf_prod_fun_image)
    1.16 - prefer 2 apply (rule injI)
    1.17 + prefer 2 apply (rule inj_onI)
    1.18  apply auto
    1.19  done
    1.20