# HG changeset patch
# User oheimb
# Date 950901896 -3600
# Node ID 87f21e25fcb63c542ed0426b0a6b5509886f9cc9
# Parent  a8d2606f49218eb37bb92bdb1afa2baf03d7a169
added Suc_le_D

diff -r a8d2606f4921 -r 87f21e25fcb6 src/HOL/Nat.ML
--- 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);