diff -r ab88297f1a56 -r 32a83e3ad5a4 arith.ML
--- a/arith.ML	Tue Mar 22 19:55:29 1994 +0100
+++ b/arith.ML	Sun Mar 27 12:36:39 1994 +0200
@@ -51,18 +51,18 @@
 val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right];
 
 (*Associative law for addition*)
-val add_assoc = prove_goal Arith.thy "m + (n + k) = (m + n) + k::nat"
+val add_assoc = prove_goal Arith.thy "(m + n) + k = m + (n + k)::nat"
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
 (*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_right_commute = prove_goal Arith.thy "(x+y)+z=(x+z)+y::nat"
+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]);
 
-val add_ac = [add_assoc, add_commute, add_right_commute];
+val add_ac = [add_assoc, add_commute, add_left_commute];
 
 
 (*** Multiplication ***)
@@ -87,17 +87,26 @@
  (fn _ => [nat_ind_tac "m" 1,
            ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
 
-val arith_ss = arith_ss addsimps [add_mult_distrib];
+(*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))]);
+
+val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2];
 
 (*Associative law for multiplication*)
-val mult_assoc = prove_goal Arith.thy "m * (n * k) = (m * n) * k::nat"
+val mult_assoc = prove_goal Arith.thy "(m * n) * k = m * (n * k)::nat"
   (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
-val mult_right_commute = prove_goal Arith.thy "(x*y)*z=(x*z)*y::nat"
+val mult_left_commute = prove_goal Arith.thy "x*(y*z) = y*(x*z)::nat"
  (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
            rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]);
 
-val mult_ac = [mult_assoc,mult_commute,mult_right_commute];
+val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
 
 (*** Difference ***)
 
@@ -105,7 +114,7 @@
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-val [prem] = goal Arith.thy "[| ~ m<n |] ==> (m-n)+n = m::nat";
+val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = m::nat";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS(asm_simp_tac arith_ss));