src/HOL/Univ.ML
changeset 4830 bd73675adbed
parent 4535 f24cebc299e4
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Univ.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/Univ.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -58,12 +58,12 @@
     1.4  by (rtac Rep_Node_inverse 1);
     1.5  qed "inj_Rep_Node";
     1.6  
     1.7 -goal Univ.thy "inj_onto Abs_Node Node";
     1.8 -by (rtac inj_onto_inverseI 1);
     1.9 +goal Univ.thy "inj_on Abs_Node Node";
    1.10 +by (rtac inj_on_inverseI 1);
    1.11  by (etac Abs_Node_inverse 1);
    1.12 -qed "inj_onto_Abs_Node";
    1.13 +qed "inj_on_Abs_Node";
    1.14  
    1.15 -val Abs_Node_inject = inj_onto_Abs_Node RS inj_ontoD;
    1.16 +val Abs_Node_inject = inj_on_Abs_Node RS inj_onD;
    1.17  
    1.18  
    1.19  (*** Introduction rules for Node ***)