# HG changeset patch
# User paulson
# Date 835259249 -7200
# Node ID ffc20ff8019045b25b5b8a3fba1178ef25b05742
# Parent  3994d37b16ae58707e3b8b3ad776de26bff88971
Restored Addsimps [Suc_le_lessD], as it cannot be added
to base HOL

diff -r 3994d37b16ae -r ffc20ff80190 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Thu Jun 20 10:26:13 1996 +0200
+++ b/src/HOL/MiniML/W.ML	Thu Jun 20 10:27:29 1996 +0200
@@ -8,14 +8,6 @@
 
 open W;
 
-
-(* stronger version of Suc_leD *)
-goalw Nat.thy [le_def] 
-        "!!m. Suc m <= n ==> m < n";
-by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (cut_facts_tac [less_linear] 1);
-by (fast_tac HOL_cs 1);
-qed "Suc_le_lessD";
 Addsimps [Suc_le_lessD];
 
 (* correctness of W with respect to has_type *)