src/HOL/Nat.ML
changeset 8260 87f21e25fcb6
parent 8115 c802042066e8
child 8423 3c19160b6432
     1.1 --- a/src/HOL/Nat.ML	Fri Feb 18 20:24:40 2000 +0100
     1.2 +++ b/src/HOL/Nat.ML	Fri Feb 18 20:24:56 2000 +0100
     1.3 @@ -57,6 +57,11 @@
     1.4  qed "not_gr0";
     1.5  AddIffs [not_gr0];
     1.6  
     1.7 +Goal "(Suc n <= m') --> (? m. m' = Suc m)";
     1.8 +by (induct_tac "m'" 1);
     1.9 +by  Auto_tac;
    1.10 +qed_spec_mp "Suc_le_D";
    1.11 +
    1.12  (*Useful in certain inductive arguments*)
    1.13  Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
    1.14  by (exhaust_tac "m" 1);