# HG changeset patch
# User berghofe
# Date 1028550606 -7200
# Node ID af96f2568406b0788d80d0f8a67ddafbeae0258e
# Parent  278f2cba42ab1d552e8a6cfe6e40a07c76ce5a0a
Removed proof of Suc_le_D (already proved in Nat.thy).

diff -r 278f2cba42ab -r af96f2568406 src/HOL/IMPP/Natural.ML
--- a/src/HOL/IMPP/Natural.ML	Mon Aug 05 14:29:20 2002 +0200
+++ b/src/HOL/IMPP/Natural.ML	Mon Aug 05 14:30:06 2002 +0200
@@ -36,11 +36,6 @@
 by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
 qed "evaln_evalc";
 
-goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)";
-by (induct_tac "m'" 1);
-by (CLASIMPSET auto_tac);
-qed_spec_mp "Suc_le_D";
-
 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";
 by (cut_facts_tac (premises()) 1);
 by (ftac Suc_le_D 1);