author | oheimb |
Fri, 18 Feb 2000 20:24:56 +0100 | |
changeset 8260 | 87f21e25fcb6 |
parent 8259 | a8d2606f4921 |
child 8261 | e4726ac0863a |
src/HOL/Nat.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Nat.ML Fri Feb 18 20:24:40 2000 +0100 +++ b/src/HOL/Nat.ML Fri Feb 18 20:24:56 2000 +0100 @@ -57,6 +57,11 @@ qed "not_gr0"; AddIffs [not_gr0]; +Goal "(Suc n <= m') --> (? m. m' = Suc m)"; +by (induct_tac "m'" 1); +by Auto_tac; +qed_spec_mp "Suc_le_D"; + (*Useful in certain inductive arguments*) Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))"; by (exhaust_tac "m" 1);