tidied

--- 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 ***)