src/HOL/Nat.ML
changeset 10558 09a91221ced1
parent 10450 60ddd5fdf93b
child 10710 0c8d58332658
     1.1 --- a/src/HOL/Nat.ML	Thu Nov 30 20:18:00 2000 +0100
     1.2 +++ b/src/HOL/Nat.ML	Fri Dec 01 11:02:55 2000 +0100
     1.3 @@ -265,13 +265,13 @@
     1.4  
     1.5  (**** Additional theorems about "less than" ****)
     1.6  
     1.7 -(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
     1.8 +(*Deleted less_natE; instead use less_imp_Suc_add RS exE*)
     1.9  Goal "m<n --> (EX k. n=Suc(m+k))";
    1.10  by (induct_tac "n" 1);
    1.11  by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
    1.12  by (blast_tac (claset() addSEs [less_SucE]
    1.13                          addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    1.14 -qed_spec_mp "less_eq_Suc_add";
    1.15 +qed_spec_mp "less_imp_Suc_add";
    1.16  
    1.17  Goal "n <= ((m + n)::nat)";
    1.18  by (induct_tac "m" 1);
    1.19 @@ -288,7 +288,7 @@
    1.20  bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
    1.21  
    1.22  Goal "(m<n) = (EX k. n=Suc(m+k))";
    1.23 -by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
    1.24 +by (blast_tac (claset() addSIs [less_add_Suc1, less_imp_Suc_add]) 1);
    1.25  qed "less_iff_Suc_add";
    1.26  
    1.27  
    1.28 @@ -634,7 +634,7 @@
    1.29  
    1.30  (*strict, in 1st argument; proof is by induction on k>0*)
    1.31  Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
    1.32 -by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
    1.33 +by (eres_inst_tac [("m1","0")] (less_imp_Suc_add RS exE) 1);
    1.34  by (Asm_simp_tac 1);
    1.35  by (induct_tac "x" 1);
    1.36  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));