Arith.ML

--- a/Arith.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/Arith.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -228,3 +228,9 @@
 
 val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
 val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
+
+goal Arith.thy "m+k<=n --> m<=n::nat";
+by(nat_ind_tac "k" 1);
+by(ALLGOALS(simp_tac arith_ss));
+by(fast_tac (HOL_cs addDs [Suc_leD]) 1);
+val plus_leD1 = result() RS mp;