Arith.ML

 (*Commutative law for addition*)  
 val add_commute = prove_goal Arith.thy "m + n = n + m::nat"
  (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];
 
 
 (*** Multiplication ***)
 

 val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right];
 
 (*Commutative law for multiplication*)
 val mult_commute = prove_goal Arith.thy "m * n = n * m::nat"
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS (asm_simp_tac arith_ss)]);
-
-(*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))]);
 
 (*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))]);