src/HOL/Nat.ML
changeset 1327 6c29cfab679c
parent 1301 42782316d510
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/Nat.ML	Sun Nov 12 13:14:13 1995 +0100
     1.2 +++ b/src/HOL/Nat.ML	Sun Nov 12 16:29:12 1995 +0100
     1.3 @@ -412,6 +412,11 @@
     1.4  by(fast_tac HOL_cs 1);
     1.5  qed "Suc_leD";
     1.6  
     1.7 +goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
     1.8 +by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
     1.9 +qed "le_SucI";
    1.10 +Addsimps[le_SucI];
    1.11 +
    1.12  goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
    1.13  by (fast_tac (HOL_cs addEs [less_asym]) 1);
    1.14  qed "less_imp_le";