HOL/Arith/add_left_commute: tidied
HOL/Arith/add_mult_distrib: DELETED DUPLICATE COPY

--- a/Arith.ML	Fri Jun 17 18:32:25 1994 +0200
+++ b/Arith.ML	Fri Jun 17 18:34:12 1994 +0200
@@ -61,9 +61,10 @@
  (fn _ =>  [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
 val add_left_commute = prove_goal Arith.thy "x+(y+z)=y+(x+z)::nat"
- (fn _ => [rtac trans 1, rtac add_commute 1, rtac trans 1,
-           rtac add_assoc 1, rtac (add_commute RS arg_cong) 1]);
+ (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
+           rtac (add_commute RS arg_cong) 1]);
 
+(*Addition is an AC-operator*)
 val add_ac = [add_assoc, add_commute, add_left_commute];
 
 
@@ -89,11 +90,6 @@
  (fn _ => [nat_ind_tac "m" 1,
            ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
 
-(*addition distributes over multiplication*)
-val add_mult_distrib = prove_goal Arith.thy "(m + n)*k = (m*k) + (n*k)::nat"
- (fn _ => [nat_ind_tac "m" 1,
-           ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
-
 val add_mult_distrib2 = prove_goal Arith.thy "k*(m + n) = (k*m) + (k*n)::nat"
  (fn _ => [nat_ind_tac "m" 1,
            ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);