src/HOL/Fun.ML
changeset 3842 b55686a7b22c
parent 3341 89fe22bf9f54
child 4059 59c1422c9da5
equal deleted inserted replaced
3841:22bbc1676768 3842:b55686a7b22c
    44 by (rtac iffI 1);
    44 by (rtac iffI 1);
    45 by (etac (major RS injD) 1);
    45 by (etac (major RS injD) 1);
    46 by (etac arg_cong 1);
    46 by (etac arg_cong 1);
    47 qed "inj_eq";
    47 qed "inj_eq";
    48 
    48 
    49 val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y";
    49 val [major] = goal Fun.thy "inj(f) ==> (@x. f(x)=f(y)) = y";
    50 by (rtac (major RS injD) 1);
    50 by (rtac (major RS injD) 1);
    51 by (rtac selectI 1);
    51 by (rtac selectI 1);
    52 by (rtac refl 1);
    52 by (rtac refl 1);
    53 qed "inj_select";
    53 qed "inj_select";
    54 
    54