src/HOL/NatDef.ML
changeset 4830 bd73675adbed
parent 4821 bfbaea156f43
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/NatDef.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -85,15 +85,15 @@
     1.4  by (rtac Rep_Nat_inverse 1);
     1.5  qed "inj_Rep_Nat";
     1.6  
     1.7 -goal thy "inj_onto Abs_Nat Nat";
     1.8 -by (rtac inj_onto_inverseI 1);
     1.9 +goal thy "inj_on Abs_Nat Nat";
    1.10 +by (rtac inj_on_inverseI 1);
    1.11  by (etac Abs_Nat_inverse 1);
    1.12 -qed "inj_onto_Abs_Nat";
    1.13 +qed "inj_on_Abs_Nat";
    1.14  
    1.15  (*** Distinctness of constructors ***)
    1.16  
    1.17  goalw thy [Zero_def,Suc_def] "Suc(m) ~= 0";
    1.18 -by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1);
    1.19 +by (rtac (inj_on_Abs_Nat RS inj_on_contraD) 1);
    1.20  by (rtac Suc_Rep_not_Zero_Rep 1);
    1.21  by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
    1.22  qed "Suc_not_Zero";
    1.23 @@ -109,7 +109,7 @@
    1.24  
    1.25  goalw thy [Suc_def] "inj(Suc)";
    1.26  by (rtac injI 1);
    1.27 -by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 1);
    1.28 +by (dtac (inj_on_Abs_Nat RS inj_onD) 1);
    1.29  by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1));
    1.30  by (dtac (inj_Suc_Rep RS injD) 1);
    1.31  by (etac (inj_Rep_Nat RS injD) 1);
    1.32 @@ -483,7 +483,7 @@
    1.33    "m=n ==> nat_rec a f m = nat_rec a f n"
    1.34    (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.35  
    1.36 -qed_goal "expand_nat_case" thy
    1.37 +qed_goal "split_nat_case" thy
    1.38    "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))"
    1.39    (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.40