Restored Addsimps [Suc_le_lessD], as it cannot be added
to base HOL

--- 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 *)