# HG changeset patch
# User lcp
# Date 806750997 -7200
# Node ID 23be92d5bf4d12ea1bf825a74a3d56e5ee470bcd
# Parent  ae58cd15e802a8188a1b3538967316b21180499b
tidied proof of add_less_mono

diff -r ae58cd15e802 -r 23be92d5bf4d src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Jul 26 10:26:19 1995 +0200
+++ b/src/HOL/Arith.ML	Wed Jul 26 11:29:57 1995 +0200
@@ -349,9 +349,9 @@
 (*strict, in both arguments*)
 goal Arith.thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l";
 by (rtac (add_less_mono1 RS less_trans) 1);
-by (REPEAT (etac asm_rl 1));
+by (REPEAT (assume_tac 1));
 by (nat_ind_tac "j" 1);
-by (ALLGOALS(asm_simp_tac arith_ss));
+by (ALLGOALS (asm_simp_tac arith_ss));
 qed "add_less_mono";
 
 (*A [clumsy] way of lifting < monotonicity to <= monotonicity *)