--- a/Arith.ML Tue Apr 19 10:50:00 1994 +0200
+++ b/Arith.ML Thu Apr 21 11:13:22 1994 +0200
@@ -241,7 +241,8 @@
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(asm_full_simp_tac arith_ss));
-by(fast_tac (HOL_cs addDs [Suc_leD]) 1);
-val plus_leD1 = result() RS mp;
+by (nat_ind_tac "k" 1);
+by (ALLGOALS (asm_simp_tac arith_ss));
+by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
+val plus_leD1_lemma = result();
+val plus_leD1 = plus_leD1_lemma RS mp;