# HG changeset patch
# User lcp
# Date 766919602 -7200
# Node ID bea4ea9128385e6a3c8d1b0dd05c583315578eb9
# Parent  14b9286ed036f116542a04ac9a8bb9a259d75c92
HOL/arith.ML/plus_leD1: tidied

diff -r 14b9286ed036 -r bea4ea912838 Arith.ML
--- 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;
diff -r 14b9286ed036 -r bea4ea912838 arith.ML
--- 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;