# HG changeset patch
# User paulson
# Date 968233686 -7200
# Node ID ae236a6dc0477ec8166dd31b71f9c721ab2dfcb7
# Parent  c7049cb55a119e279b4d6ab6245f802685f7817a
tidied

diff -r c7049cb55a11 -r ae236a6dc047 src/ZF/ArithSimp.ML
--- a/src/ZF/ArithSimp.ML	Wed Sep 06 11:47:37 2000 +0200
+++ b/src/ZF/ArithSimp.ML	Wed Sep 06 11:48:06 2000 +0200
@@ -285,13 +285,11 @@
 (**** Additional theorems about "le" ****)
 
 Goal "m:nat ==> m le (m #+ n)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
+by (Asm_simp_tac 1);
 qed "add_le_self";
 
 Goal "m:nat ==> m le (n #+ m)";
-by (stac add_commute 1);
-by (etac add_le_self 1);
+by (Asm_simp_tac 1);
 qed "add_le_self2";
 
 (*** Monotonicity of Multiplication ***)