New arithmetic laws let us delete three lines of a proof

--- a/src/HOL/MiniML/W.ML	Tue May 20 11:41:26 1997 +0200
+++ b/src/HOL/MiniML/W.ML	Tue May 20 11:41:56 1997 +0200
@@ -253,9 +253,6 @@
 by (etac exE 1);
 by (rotate_tac 3 1);
 by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
-by (dtac add_lessD1 1);
-by (fast_tac (!claset addIs [less_irrefl]) 1);
 (* case Abs e *)
 by (asm_full_simp_tac (!simpset addsimps
     [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);