# HG changeset patch
# User webertj
# Date 1350831853 -7200
# Node ID 326f87427719856afb9702c35c5207bde240a22c
# Parent  1167c1157a5b83b05bd259adb7ee9b7729d98303# Parent  a8cc904a682087f792969668379e9d9d85480bb1
merged

diff -r 1167c1157a5b -r 326f87427719 NEWS
--- a/NEWS	Sun Oct 21 16:43:08 2012 +0200
+++ b/NEWS	Sun Oct 21 17:04:13 2012 +0200
@@ -79,7 +79,6 @@
 written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
 accordingly.
 
-
 * Theory "Library/Multiset":
 
   - Renamed constants
@@ -145,6 +144,13 @@
 
     INCOMPATIBILITY.
 
+* HOL/Rings: renamed lemmas
+
+left_distrib ~> distrib_right
+right_distrib ~> distrib_left
+
+in class semiring.  INCOMPATIBILITY.
+
 * HOL/BNF: New (co)datatype package based on bounded natural
 functors with support for mixed, nested recursion and interesting
 non-free datatypes.
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -35,7 +35,7 @@
   apply (rule abelian_groupI, simp_all)
   defer 1
   apply (rule comm_monoidI, simp_all)
- apply (rule left_distrib)
+ apply (rule distrib_right)
 apply (fast intro: left_minus)
 done
 
@@ -165,7 +165,7 @@
     and "a_inv \<Z> x = - x"
     and "a_minus \<Z> x y = x - y"
 proof -
-  show "domain \<Z>" by unfold_locales (auto simp: left_distrib right_distrib)
+  show "domain \<Z>" by unfold_locales (auto simp: distrib_right distrib_left)
 qed (simp
     add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -1818,7 +1818,7 @@
 
 lemma INTEG_cring: "cring INTEG"
   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
-    left_minus left_distrib)
+    left_minus distrib_right)
 
 lemma INTEG_id_eval:
   "UP_pre_univ_prop INTEG INTEG id"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -699,7 +699,7 @@
   proof induct
     case empty thus ?case by simp
   next
-    case (insert x A) thus ?case by (simp add: right_distrib)
+    case (insert x A) thus ?case by (simp add: distrib_left)
   qed
 next
   case False thus ?thesis by (simp add: setsum_def)
@@ -713,7 +713,7 @@
   proof induct
     case empty thus ?case by simp
   next
-    case (insert x A) thus ?case by (simp add: left_distrib)
+    case (insert x A) thus ?case by (simp add: distrib_right)
   qed
 next
   case False thus ?thesis by (simp add: setsum_def)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -153,7 +153,7 @@
   "n < m \<longleftrightarrow> nat_of n < nat_of m"
 
 instance proof
-qed (auto simp add: code_numeral left_distrib intro: mult_commute)
+qed (auto simp add: code_numeral distrib_right intro: mult_commute)
 
 end
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Complex.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -141,7 +141,7 @@
 
 instance
   by intro_classes (simp_all add: complex_mult_def
-    right_distrib left_distrib right_diff_distrib left_diff_distrib
+    distrib_left distrib_right right_diff_distrib left_diff_distrib
     complex_inverse_def complex_divide_def
     power2_eq_square add_divide_distrib [symmetric]
     complex_eq_iff)
@@ -206,9 +206,9 @@
 proof
   fix a b :: real and x y :: complex
   show "scaleR a (x + y) = scaleR a x + scaleR a y"
-    by (simp add: complex_eq_iff right_distrib)
+    by (simp add: complex_eq_iff distrib_left)
   show "scaleR (a + b) x = scaleR a x + scaleR b x"
-    by (simp add: complex_eq_iff left_distrib)
+    by (simp add: complex_eq_iff distrib_right)
   show "scaleR a (scaleR b x) = scaleR (a * b) x"
     by (simp add: complex_eq_iff mult_assoc)
   show "scaleR 1 x = x"
@@ -297,7 +297,7 @@
        (simp add: real_sqrt_sum_squares_triangle_ineq)
   show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
     by (induct x)
-       (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
+       (simp add: power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
   show "norm (x * y) = norm x * norm y"
     by (induct x, induct y)
        (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
@@ -730,7 +730,7 @@
     unfolding z b_def rcis_def using `r \<noteq> 0`
     by (simp add: of_real_def sgn_scaleR sgn_if, simp add: cis_def)
   have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
-    by (induct_tac n, simp_all add: right_distrib cis_mult [symmetric],
+    by (induct_tac n, simp_all add: distrib_left cis_mult [symmetric],
       simp add: cis_def)
   have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
     by (case_tac x rule: int_diff_cases,
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -305,7 +305,7 @@
   finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ `0 < real x`] by auto
   also have "\<dots> \<le> (?b + (float_divr prec x ?b))/2" by (rule divide_right_mono, auto simp add: float_divr)
   also have "\<dots> = (Float 1 -1) * (?b + (float_divr prec x ?b))" by simp
-  finally show ?case unfolding sqrt_iteration.simps Let_def right_distrib .
+  finally show ?case unfolding sqrt_iteration.simps Let_def distrib_left .
 qed
 
 lemma sqrt_iteration_lower_bound: assumes "0 < real x"
@@ -955,7 +955,7 @@
       using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
       unfolding sin_coeff_def by auto
 
-    have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add left_distrib right_distrib by auto
+    have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
     moreover
     have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
     hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
@@ -1173,7 +1173,7 @@
 proof (induct n arbitrary: x)
   case (Suc n)
   have split_pi_off: "x + (Suc n) * (2 * pi) = (x + n * (2 * pi)) + 2 * pi"
-    unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
+    unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
   show ?case unfolding split_pi_off using Suc by auto
 qed auto
 
@@ -1714,7 +1714,7 @@
 lemma ln_add: assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
 proof -
   have "x \<noteq> 0" using assms by auto
-  have "x + y = x * (1 + y / x)" unfolding right_distrib times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
+  have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
   moreover
   have "0 < y / x" using assms divide_pos_pos by auto
   hence "0 < 1 + y / x" by auto
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -413,7 +413,7 @@
 apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
  apply (case_tac "n1 = n2")
   apply(simp_all add: algebra_simps)
-apply(simp add: left_distrib[symmetric])
+apply(simp add: distrib_right[symmetric])
 done
 
 lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
@@ -727,7 +727,7 @@
       by (simp add: Let_def split_def)
     from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
     from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
-    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: left_distrib)
+    also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
   finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
   with th2 th have ?case using m0 by blast} 
 ultimately show ?case by blast
@@ -754,7 +754,7 @@
   with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
   from th3[simplified] th2[simplified] th[simplified] show ?case 
-    by (simp add: left_distrib)
+    by (simp add: distrib_right)
 next
   case (6 s t n a)
   let ?ns = "fst (zsplit0 s)"
@@ -779,7 +779,7 @@
     by (simp add: Let_def split_def)
   from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
-  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
+  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
   finally show ?case using th th2 by simp
 qed
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -569,7 +569,7 @@
 apply (induct t s rule: numadd.induct, simp_all add: Let_def)
 apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
 apply (case_tac "n1 = n2", simp_all add: algebra_simps)
-by (simp only: left_distrib[symmetric],simp)
+by (simp only: distrib_right[symmetric],simp)
 
 lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
 by (induct t s rule: numadd.induct, auto simp add: Let_def)
@@ -937,7 +937,7 @@
     by (simp add: Let_def split_def algebra_simps)
   also have "\<dots> = Inum bs a + Inum bs b" using 2 by (cases "rsplit0 a") auto
   finally show ?case using nb by simp 
-qed (auto simp add: Let_def split_def algebra_simps, simp add: right_distrib[symmetric])
+qed (auto simp add: Let_def split_def algebra_simps, simp add: distrib_left[symmetric])
 
     (* Linearize a formula*)
 definition
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -743,11 +743,11 @@
 apply (induct t s rule: numadd.induct, simp_all add: Let_def)
  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   apply (case_tac "n1 = n2", simp_all add: algebra_simps)
-  apply (simp only: left_distrib[symmetric])
+  apply (simp only: distrib_right[symmetric])
  apply simp
 apply (case_tac "lex_bnd t1 t2", simp_all)
  apply (case_tac "c1+c2 = 0")
-  by (case_tac "t1 = t2", simp_all add: algebra_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib)
+  by (case_tac "t1 = t2", simp_all add: algebra_simps distrib_right[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add distrib_right)
 
 lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
 by (induct t s rule: numadd.induct, auto simp add: Let_def)
@@ -1493,7 +1493,7 @@
   with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   from abjs 6  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
   from th3[simplified] th2[simplified] th[simplified] show ?case 
-    by (simp add: left_distrib)
+    by (simp add: distrib_right)
 next
   case (7 s t n a)
   let ?ns = "fst (zsplit0 s)"
@@ -1518,7 +1518,7 @@
     by (simp add: Let_def split_def)
   from abj 8 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   hence "?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp
-  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)
+  also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
   finally show ?case using th th2 by simp
 next
   case (9 t n a)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -224,7 +224,7 @@
 apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
 apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
 apply (case_tac "n1 = n2", simp_all add: field_simps)
-apply (simp only: right_distrib[symmetric]) 
+apply (simp only: distrib_left[symmetric]) 
 by (auto simp del: polyadd simp add: polyadd[symmetric])
 
 lemma tmadd_nb0[simp]: "\<lbrakk> tmbound0 t ; tmbound0 s\<rbrakk> \<Longrightarrow> tmbound0 (tmadd (t,s))"
@@ -358,7 +358,7 @@
   apply (simp add: Let_def split_def field_simps)
   apply (simp add: Let_def split_def field_simps)
   apply (simp add: Let_def split_def field_simps)
-  apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric])
+  apply (simp add: Let_def split_def mult_assoc distrib_left[symmetric])
   apply (simp add: Let_def split_def field_simps)
   apply (simp add: Let_def split_def field_simps)
   done
@@ -1933,7 +1933,7 @@
     also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) = 0"
       using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
     also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r= 0"
-      by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
+      by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
     
     also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0" using d by simp 
     finally have ?thesis using c d 
@@ -1947,7 +1947,7 @@
     also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) = 0" 
       using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
     also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r= 0"
-      by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
+      by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
     also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r = 0" using c by simp 
     finally have ?thesis using c d 
       by (simp add: r[of "- (?t/ (2*?c))"] msubsteq_def Let_def evaldjf_ex)
@@ -1964,7 +1964,7 @@
       using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r =0" 
       using nonzero_mult_divide_cancel_left [OF dc] c d
-      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally  have ?thesis using c d 
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps)
   }
@@ -2015,7 +2015,7 @@
     also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0" 
       using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
     also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
-      by (simp add: field_simps right_distrib[of "2*?d"] del: right_distrib)
+      by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
     
     also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r \<noteq> 0" using d by simp 
     finally have ?thesis using c d 
@@ -2029,7 +2029,7 @@
     also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0" 
       using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
     also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
-      by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
+      by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
     also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0" using c by simp 
     finally have ?thesis using c d 
       by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
@@ -2046,7 +2046,7 @@
       using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0" 
       using nonzero_mult_divide_cancel_left[OF dc] c d
-      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally  have ?thesis using c d 
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps)
   }
@@ -2112,7 +2112,7 @@
       using dc' dc'' mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0" 
       using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
-      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally  have ?thesis using dc c d  nc nd dc'
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) 
   }
@@ -2134,7 +2134,7 @@
       using dc' order_less_not_sym[OF dc'] mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r < 0" 
       using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
-      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally  have ?thesis using dc c d  nc nd
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) 
   }
@@ -2149,7 +2149,7 @@
       using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
     also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r < 0" 
       using nonzero_mult_divide_cancel_left[OF c'] c
-      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
     finally have ?thesis using c d nc nd 
       by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   }
@@ -2163,7 +2163,7 @@
       using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0" 
       using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
-        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
+        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
     finally have ?thesis using c d nc nd 
       by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   }
@@ -2179,7 +2179,7 @@
       using d mult_less_cancel_left_disj[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
     also have "\<dots> \<longleftrightarrow> - ?a*?s+  2*?d *?r < 0" 
       using nonzero_mult_divide_cancel_left[OF d'] d
-      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
     finally have ?thesis using c d nc nd 
       by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   }
@@ -2193,7 +2193,7 @@
       using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a*?s -  2*?d *?r < 0" 
       using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
-        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
+        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
     finally have ?thesis using c d nc nd 
       by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   }
@@ -2258,7 +2258,7 @@
       using dc' dc'' mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r <= 0" 
       using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
-      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally  have ?thesis using dc c d  nc nd dc'
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) 
   }
@@ -2280,7 +2280,7 @@
       using dc' order_less_not_sym[OF dc'] mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r <= 0" 
       using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
-      by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
     finally  have ?thesis using dc c d  nc nd
       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) 
   }
@@ -2295,7 +2295,7 @@
       using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
     also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r <= 0" 
       using nonzero_mult_divide_cancel_left[OF c'] c
-      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
     finally have ?thesis using c d nc nd 
       by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   }
@@ -2309,7 +2309,7 @@
       using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r <= 0" 
       using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
-        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
+        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
     finally have ?thesis using c d nc nd 
       by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   }
@@ -2325,7 +2325,7 @@
       using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
     also have "\<dots> \<longleftrightarrow> - ?a*?s+  2*?d *?r <= 0" 
       using nonzero_mult_divide_cancel_left[OF d'] d
-      by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
+      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
     finally have ?thesis using c d nc nd 
       by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   }
@@ -2339,7 +2339,7 @@
       using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] by simp
     also have "\<dots> \<longleftrightarrow> ?a*?s -  2*?d *?r <= 0" 
       using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
-        by (simp add: algebra_simps diff_divide_distrib del:  left_distrib)
+        by (simp add: algebra_simps diff_divide_distrib del:  distrib_right)
     finally have ?thesis using c d nc nd 
       by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
   }
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -128,7 +128,7 @@
      "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
 apply (induct "p", simp, clarify) 
 apply (case_tac "q")
-apply (simp_all add: right_distrib)
+apply (simp_all add: distrib_left)
 done
 
 lemma pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
@@ -142,13 +142,13 @@
 apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x")
 apply (induct_tac [2] "p1", auto)
 apply (case_tac "p2")
-apply (auto simp add: right_distrib)
+apply (auto simp add: distrib_left)
 done
 
 lemma poly_cmult: "poly (c %* p) x = c * poly p x"
 apply (induct "p") 
 apply (case_tac [2] "x=0")
-apply (auto simp add: right_distrib mult_ac)
+apply (auto simp add: distrib_left mult_ac)
 done
 
 lemma poly_minus: "poly (-- p) x = - (poly p x)"
@@ -162,7 +162,7 @@
 apply (induct "p1")
 apply (auto simp add: poly_cmult)
 apply (case_tac p1)
-apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac)
+apply (auto simp add: poly_cmult poly_add distrib_right distrib_left mult_ac)
 done
 
 lemma poly_exp: "poly (p %^ n) (x::'a::comm_ring_1) = (poly p x) ^ n"
@@ -206,7 +206,7 @@
 
 
 lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))"
-apply (auto simp add: poly_add poly_cmult right_distrib)
+apply (auto simp add: poly_add poly_cmult distrib_left)
 apply (case_tac "p", simp) 
 apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
 apply (case_tac "q", auto)
@@ -408,7 +408,7 @@
 by (auto simp add: field_simps poly_add poly_minus_def fun_eq poly_cmult)
 
 lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
-by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib)
+by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
 
 lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly ([]::('a::{idom, ring_char_0}) list) | poly q = poly r)"
 apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst])
@@ -464,9 +464,9 @@
 text{*Basics of divisibility.*}
 
 lemma poly_primes: "([a, (1::'a::idom)] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
-apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
+apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult distrib_right [symmetric])
 apply (drule_tac x = "-a" in spec)
-apply (auto simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
+apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
 apply (rule_tac x = "qa *** q" in exI)
 apply (rule_tac [2] x = "p *** qa" in exI)
 apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
@@ -501,7 +501,7 @@
    "[| p divides q; p divides r |] ==> p divides (q +++ r)"
 apply (simp add: divides_def, auto)
 apply (rule_tac x = "qa +++ qaa" in exI)
-apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
+apply (auto simp add: poly_add fun_eq poly_mult distrib_left)
 done
 
 lemma poly_divides_diff:
@@ -557,7 +557,7 @@
 apply (unfold divides_def)
 apply (rule_tac x = q in exI)
 apply (induct_tac "n", simp)
-apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
+apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
 apply safe
 apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)") 
 apply simp 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -304,7 +304,7 @@
 qed auto
 
 lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
-by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
+by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
 
 lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
   using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -66,7 +66,7 @@
     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
       by (simp add: algebra_simps)
   finally have "a = a div b * b + (a + c * b) mod b"
-    by (simp add: add_commute [of a] add_assoc left_distrib)
+    by (simp add: add_commute [of a] add_assoc distrib_right)
   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
     by (simp add: mod_div_equality)
   then show ?thesis by simp
@@ -1274,9 +1274,9 @@
  prefer 2 apply (simp add: right_diff_distrib)
 apply (subgoal_tac "0 < b * (1 + q - q') ")
 apply (erule_tac [2] order_le_less_trans)
- prefer 2 apply (simp add: right_diff_distrib right_distrib)
+ prefer 2 apply (simp add: right_diff_distrib distrib_left)
 apply (subgoal_tac "b * q' < b * (1 + q) ")
- prefer 2 apply (simp add: right_diff_distrib right_distrib)
+ prefer 2 apply (simp add: right_diff_distrib distrib_left)
 apply (simp add: mult_less_cancel_left)
 done
 
@@ -1332,11 +1332,11 @@
   apply (induct a b rule: posDivAlg.induct)
   apply auto
   apply (simp add: divmod_int_rel_def)
-  apply (subst posDivAlg_eqn, simp add: right_distrib)
+  apply (subst posDivAlg_eqn, simp add: distrib_left)
   apply (case_tac "a < b")
   apply simp_all
   apply (erule splitE)
-  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
+  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
   done
 
 
@@ -1366,7 +1366,7 @@
   apply (case_tac "a + b < (0\<Colon>int)")
   apply simp_all
   apply (erule splitE)
-  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
+  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
   done
 
 
@@ -1732,7 +1732,7 @@
      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
 apply (subgoal_tac "0 < b'* (q' + 1) ")
  apply (simp add: zero_less_mult_iff)
-apply (simp add: right_distrib)
+apply (simp add: distrib_left)
 done
 
 lemma zdiv_mono2_lemma:
@@ -1744,7 +1744,7 @@
  apply (simp add: mult_less_cancel_left)
 apply (subgoal_tac "b*q = r' - r + b'*q'")
  prefer 2 apply simp
-apply (simp (no_asm_simp) add: right_distrib)
+apply (simp (no_asm_simp) add: distrib_left)
 apply (subst add_commute, rule add_less_le_mono, arith)
 apply (rule mult_right_mono, auto)
 done
@@ -1773,7 +1773,7 @@
 apply (frule q_neg_lemma, assumption+) 
 apply (subgoal_tac "b*q' < b* (q + 1) ")
  apply (simp add: mult_less_cancel_left)
-apply (simp add: right_distrib)
+apply (simp add: distrib_left)
 apply (subgoal_tac "b*q' \<le> b'*q'")
  prefer 2 apply (simp add: mult_right_mono_neg, arith)
 done
@@ -1795,7 +1795,7 @@
 lemma zmult1_lemma:
      "[| divmod_int_rel b c (q, r) |]  
       ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
-by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib mult_ac)
+by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left mult_ac)
 
 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
 apply (case_tac "c = 0", simp)
@@ -1807,7 +1807,7 @@
 lemma zadd1_lemma:
      "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
       ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
-by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib)
+by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
 
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma zdiv_zadd1_eq:
@@ -1900,7 +1900,7 @@
 lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
 by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
-                   zero_less_mult_iff right_distrib [symmetric] 
+                   zero_less_mult_iff distrib_left [symmetric] 
                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
 
 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/GCD.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -1199,7 +1199,7 @@
           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
             by simp
           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
-            by (simp only: mult_assoc right_distrib)
+            by (simp only: mult_assoc distrib_left)
           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
             by algebra
           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -411,7 +411,7 @@
       from x y have "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
       with a have " \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
         by (simp add: mult_left_mono)
-      also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib)
+      also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: distrib_left)
       also have "\<dots> = p x + p y" by (simp only: p_def)
       finally show ?thesis .
     qed
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -140,7 +140,7 @@
         also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
           by simp
         also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
-          by (simp add: left_distrib)
+          by (simp add: distrib_right)
         also from h'_def x1_rep E HE y1 x0
         have "h y1 + a1 * xi = h' x1"
           by (rule h'_definite [symmetric])
@@ -179,7 +179,7 @@
         also from y1 have "h (c \<cdot> y1) = c * h y1"
           by simp
         also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
-          by (simp only: right_distrib)
+          by (simp only: distrib_left)
         also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
           by (rule h'_definite [symmetric])
         finally show ?thesis .
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Int.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -136,7 +136,7 @@
      "(i::int)<j ==> 0<k ==> int k * i < int k * j"
 apply (induct k)
 apply simp
-apply (simp add: left_distrib)
+apply (simp add: distrib_right)
 apply (case_tac "k=0")
 apply (simp_all add: add_strict_mono)
 done
@@ -193,8 +193,8 @@
 done
 
 lemmas int_distrib =
-  left_distrib [of z1 z2 w]
-  right_distrib [of w z1 z2]
+  distrib_right [of z1 z2 w]
+  distrib_left [of w z1 z2]
   left_diff_distrib [of z1 z2 w]
   right_diff_distrib [of w z1 z2]
   for z1 z2 w :: int
@@ -499,7 +499,7 @@
 lemma even_less_0_iff:
   "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
 proof -
-  have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib del: one_add_one)
+  have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one)
   also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
     by (simp add: mult_less_0_iff zero_less_two 
                   order_less_not_sym [OF zero_less_two])
@@ -1097,8 +1097,8 @@
 
 text{*These distributive laws move literals inside sums and differences.*}
 
-lemmas left_distrib_numeral [simp] = left_distrib [of _ _ "numeral v"] for v
-lemmas right_distrib_numeral [simp] = right_distrib [of "numeral v"] for v
+lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
+lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
 lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
 lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -196,7 +196,7 @@
     by (simp split: enat.split)
   show "(a + b) * c = a * c + b * c"
     unfolding times_enat_def zero_enat_def
-    by (simp split: enat.split add: left_distrib)
+    by (simp split: enat.split add: distrib_right)
   show "0 * a = 0"
     unfolding times_enat_def zero_enat_def
     by (simp split: enat.split)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -260,11 +260,11 @@
 proof
   fix a b c :: "'a fps"
   show "(a + b) * c = a * c + b * c"
-    by (simp add: expand_fps_eq fps_mult_nth left_distrib setsum_addf)
+    by (simp add: expand_fps_eq fps_mult_nth distrib_right setsum_addf)
 next
   fix a b c :: "'a fps"
   show "a * (b + c) = a * b + a * c"
-    by (simp add: expand_fps_eq fps_mult_nth right_distrib setsum_addf)
+    by (simp add: expand_fps_eq fps_mult_nth distrib_left setsum_addf)
 qed
 
 instance fps :: (semiring_0) semiring_0
@@ -363,10 +363,10 @@
 instance fps :: (ring) ring ..
 
 instance fps :: (ring_1) ring_1
-  by (intro_classes, auto simp add: diff_minus left_distrib)
+  by (intro_classes, auto simp add: diff_minus distrib_right)
 
 instance fps :: (comm_ring_1) comm_ring_1
-  by (intro_classes, auto simp add: diff_minus left_distrib)
+  by (intro_classes, auto simp add: diff_minus distrib_right)
 
 instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors
 proof
@@ -3200,7 +3200,7 @@
   show ?thesis
     using fps_sin_cos_sum_of_squares[of c]
     apply (simp add: fps_tan_def fps_divide_deriv[OF th0] fps_sin_deriv fps_cos_deriv add: fps_const_neg[symmetric] field_simps power2_eq_square del: fps_const_neg)
-    unfolding right_distrib[symmetric]
+    unfolding distrib_left[symmetric]
     by simp
 qed
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -55,7 +55,7 @@
     apply (rule f.pos_bounded [THEN exE], rename_tac Kf)
     apply (rule g.pos_bounded [THEN exE], rename_tac Kg)
     apply (rule_tac x="Kf + Kg" in exI, safe)
-    apply (subst right_distrib)
+    apply (subst distrib_left)
     apply (rule order_trans [OF norm_triangle_ineq])
     apply (rule add_mono, erule spec, erule spec)
     done
@@ -413,8 +413,8 @@
  apply (induct n)
   apply (simp add: FDERIV_ident)
  apply (drule FDERIV_mult [OF FDERIV_ident])
- apply (simp only: of_nat_Suc left_distrib mult_1_left)
- apply (simp only: power_Suc right_distrib add_ac mult_ac)
+ apply (simp only: of_nat_Suc distrib_right mult_1_left)
+ apply (simp only: power_Suc distrib_left add_ac mult_ac)
 done
 
 lemma FDERIV_power:
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -238,7 +238,7 @@
     have th4: "cmod (complex_of_real (cmod b) / b) *
    cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
    < cmod (complex_of_real (cmod b) / b) * 1"
-      apply (simp only: norm_mult[symmetric] right_distrib)
+      apply (simp only: norm_mult[symmetric] distrib_left)
       using b v by (simp add: th2)
 
     from mult_less_imp_less_left[OF th4 th3]
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -201,7 +201,7 @@
   show "inner x y = inner y x"
     unfolding inner_real_def by (rule mult_commute)
   show "inner (x + y) z = inner x z + inner y z"
-    unfolding inner_real_def by (rule left_distrib)
+    unfolding inner_real_def by (rule distrib_right)
   show "inner (scaleR r x) y = r * inner x y"
     unfolding inner_real_def real_scaleR_def by (rule mult_assoc)
   show "0 \<le> inner x x"
@@ -225,9 +225,9 @@
   show "inner x y = inner y x"
     unfolding inner_complex_def by (simp add: mult_commute)
   show "inner (x + y) z = inner x z + inner y z"
-    unfolding inner_complex_def by (simp add: left_distrib)
+    unfolding inner_complex_def by (simp add: distrib_right)
   show "inner (scaleR r x) y = r * inner x y"
-    unfolding inner_complex_def by (simp add: right_distrib)
+    unfolding inner_complex_def by (simp add: distrib_left)
   show "0 \<le> inner x x"
     unfolding inner_complex_def by simp
   show "inner x x = 0 \<longleftrightarrow> x = 0"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -141,13 +141,13 @@
   show "c * a \<le> c * b"
   proof (rule ord_intro)
     from `a \<le> b` have "c * (a + b) = c * b" by simp
-    thus "c * a + c * b = c * b" by (simp add: right_distrib)
+    thus "c * a + c * b = c * b" by (simp add: distrib_left)
   qed
 
   show "a * c \<le> b * c"
   proof (rule ord_intro)
     from `a \<le> b` have "(a + b) * c = b * c" by simp
-    thus "a * c + b * c = b * c" by (simp add: left_distrib)
+    thus "a * c + b * c = b * c" by (simp add: distrib_right)
   qed
 qed
 
@@ -206,7 +206,7 @@
 by (metis less_add(2) star_unfold_left)
 
 lemma star_mult_idem [simp]: "star x * star x = star x"
-by (metis add_commute add_est1 eq_iff mult_1_right right_distrib star3 star_unfold_left)
+by (metis add_commute add_est1 eq_iff mult_1_right distrib_left star3 star_unfold_left)
 
 lemma less_star [simp]: "x \<le> star x"
 by (metis less_add(2) mult_1_right mult_left_mono one_less_star order_trans star_unfold_left zero_minimum)
@@ -232,7 +232,7 @@
   thus "x + star b * x * a \<le> x + star b * b * x"
     using add_mono by auto
   show "\<dots> \<le> star b * x"
-    by (metis add_supremum left_distrib less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
+    by (metis add_supremum distrib_right less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
 qed
 
 lemma star_simulation [simp]:
@@ -273,10 +273,10 @@
 by (metis add_commute ord_simp star_idemp star_mono star_mult_idem star_one star_unfold_left)
 
 lemma star_unfold2: "star x * y = y + x * star x * y"
-by (subst star_unfold_right[symmetric]) (simp add: mult_assoc left_distrib)
+by (subst star_unfold_right[symmetric]) (simp add: mult_assoc distrib_right)
 
 lemma star_absorb_one [simp]: "star (x + 1) = star x"
-by (metis add_commute eq_iff left_distrib less_add mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star)
+by (metis add_commute eq_iff distrib_right less_add mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star)
 
 lemma star_absorb_one' [simp]: "star (1 + x) = star x"
 by (subst add_commute) (fact star_absorb_one)
@@ -292,13 +292,13 @@
 
 lemma ka18: "(x * star x) * star (y * star x) + (y * star x) * star (y * star x)
   \<le> star x * star (y * star x)"
-by (metis ka16 ka17 left_distrib mult_assoc plus_leI)
+by (metis ka16 ka17 distrib_right mult_assoc plus_leI)
 
 lemma star_decomp: "star (x + y) = star x * star (y * star x)"
 proof (rule antisym)
   have "1 + (x + y) * star x * star (y * star x) \<le>
     1 + x * star x * star (y * star x) + y * star x * star (y * star x)"
-    by (metis add_commute add_left_commute eq_iff left_distrib mult_assoc)
+    by (metis add_commute add_left_commute eq_iff distrib_right mult_assoc)
   also have "\<dots> \<le> star x * star (y * star x)"
     by (metis add_commute add_est1 add_left_commute ka18 plus_leI star_unfold_left x_less_star)
   finally show "star (x + y) \<le> star x * star (y * star x)"
@@ -342,7 +342,7 @@
 by (metis add_commute ka27)
 
 lemma ka29: "(y * (1 + x) \<le> (1 + x) * star y) = (y * x \<le> (1 + x) * star y)"
-by (metis add_supremum left_distrib less_add(1) less_star mult.left_neutral mult.right_neutral order_trans right_distrib)
+by (metis add_supremum distrib_right less_add(1) less_star mult.left_neutral mult.right_neutral order_trans distrib_left)
 
 lemma ka30: "star x * star y \<le> star (x + y)"
 by (metis mult_left_mono star_decomp star_mono x_less_star zero_minimum)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/ListVector.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -94,7 +94,7 @@
 apply(simp)
 apply(case_tac zs)
  apply(simp)
-apply(simp add:add_assoc)
+apply(simp add: add_assoc)
 done
 
 subsection "Inner product"
@@ -103,13 +103,13 @@
 "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
 
 lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
-by(simp add:iprod_def)
+by(simp add: iprod_def)
 
 lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
-by(simp add:iprod_def)
+by(simp add: iprod_def)
 
 lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
-by(simp add:iprod_def)
+by(simp add: iprod_def)
 
 lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
 apply(induct cs arbitrary:xs)
@@ -128,7 +128,7 @@
 apply simp
 apply(case_tac zs)
 apply (simp)
-apply(simp add:left_distrib)
+apply(simp add: distrib_right)
 done
 
 lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
@@ -138,7 +138,7 @@
 apply simp
 apply(case_tac zs)
 apply (simp)
-apply(simp add:left_diff_distrib)
+apply(simp add: left_diff_distrib)
 done
 
 lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
@@ -146,7 +146,7 @@
 apply simp
 apply(case_tac ys)
 apply (simp)
-apply (simp add:right_distrib mult_assoc)
+apply (simp add: distrib_left mult_assoc)
 done
 
-end
\ No newline at end of file
+end
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/Polynomial.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -975,7 +975,7 @@
   assume "y \<noteq> 0"
   hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
     using pdivmod_rel [of x y]
-    by (simp add: pdivmod_rel_def left_distrib)
+    by (simp add: pdivmod_rel_def distrib_right)
   thus "(x + z * y) div y = z + x div y"
     by (rule div_poly_eq)
 next
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -421,7 +421,7 @@
   show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
     unfolding norm_prod_def
     apply (simp add: power_mult_distrib)
-    apply (simp add: right_distrib [symmetric])
+    apply (simp add: distrib_left [symmetric])
     apply (simp add: real_sqrt_mult_distrib)
     done
   show "sgn x = scaleR (inverse (norm x)) x"
@@ -475,7 +475,7 @@
     apply (rule allI)
     apply (simp add: norm_Pair)
     apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
-    apply (simp add: right_distrib)
+    apply (simp add: distrib_left)
     apply (rule add_mono [OF norm_f norm_g])
     done
   then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
@@ -528,7 +528,7 @@
     by (simp add: inner_add_left)
   show "inner (scaleR r x) y = r * inner x y"
     unfolding inner_prod_def
-    by (simp add: right_distrib)
+    by (simp add: distrib_left)
   show "0 \<le> inner x x"
     unfolding inner_prod_def
     by (intro add_nonneg_nonneg inner_ge_zero)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -125,7 +125,7 @@
 
 lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
 apply (induct p arbitrary: q, simp)
-apply (case_tac q, simp_all add: right_distrib)
+apply (case_tac q, simp_all add: distrib_left)
 done
 
 lemma (in ring_1) pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
@@ -141,17 +141,17 @@
   case Nil thus ?case by simp
 next
   case (Cons a as p2) thus ?case
-    by (cases p2, simp_all  add: add_ac right_distrib)
+    by (cases p2, simp_all  add: add_ac distrib_left)
 qed
 
 lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
 apply (induct "p")
 apply (case_tac [2] "x=zero")
-apply (auto simp add: right_distrib mult_ac)
+apply (auto simp add: distrib_left mult_ac)
 done
 
 lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x"
-  by (induct p, auto simp add: right_distrib mult_ac)
+  by (induct p, auto simp add: distrib_left mult_ac)
 
 lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
 apply (simp add: poly_minus_def)
@@ -164,7 +164,7 @@
 next
   case (Cons a as p2)
   thus ?case by (cases as,
-    simp_all add: poly_cmult poly_add left_distrib right_distrib mult_ac)
+    simp_all add: poly_cmult poly_add distrib_right distrib_left mult_ac)
 qed
 
 class idom_char_0 = idom + ring_char_0
@@ -394,7 +394,7 @@
 by (auto simp add: algebra_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric])
 
 lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
-by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric])
+by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left minus_mult_left[symmetric] minus_mult_right[symmetric])
 
 subclass (in idom_char_0) comm_ring_1 ..
 lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
@@ -458,9 +458,9 @@
 text{*Basics of divisibility.*}
 
 lemma (in idom) poly_primes: "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
-apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
+apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult distrib_right [symmetric])
 apply (drule_tac x = "uminus a" in spec)
-apply (simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
+apply (simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
 apply (cases "p = []")
 apply (rule exI[where x="[]"])
 apply simp
@@ -471,10 +471,10 @@
 apply (cases "\<exists>q\<Colon>'a list. p = a %* q +++ ((0\<Colon>'a) # q)")
 apply (clarsimp simp add: poly_add poly_cmult)
 apply (rule_tac x="qa" in exI)
-apply (simp add: left_distrib [symmetric])
+apply (simp add: distrib_right [symmetric])
 apply clarsimp
 
-apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
+apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
 apply (rule_tac x = "pmult qa q" in exI)
 apply (rule_tac [2] x = "pmult p qa" in exI)
 apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
@@ -509,7 +509,7 @@
    "[| p divides q; p divides r |] ==> p divides (q +++ r)"
 apply (simp add: divides_def, auto)
 apply (rule_tac x = "padd qa qaa" in exI)
-apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
+apply (auto simp add: poly_add fun_eq poly_mult distrib_left)
 done
 
 lemma (in comm_ring_1) poly_divides_diff:
@@ -605,7 +605,7 @@
 apply (unfold divides_def)
 apply (rule_tac x = q in exI)
 apply (induct_tac "n", simp)
-apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
+apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
 apply safe
 apply (subgoal_tac "?poly (?mulexp n [uminus a, one] q) \<noteq> ?poly (pmult (?pexp [uminus a, one] (Suc n)) qa)")
 apply simp
@@ -948,7 +948,7 @@
   case (Suc n a p)
   have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))"
     apply (rule ext, simp add: poly_mult poly_add poly_cmult)
-    by (simp add: mult_ac add_ac right_distrib)
+    by (simp add: mult_ac add_ac distrib_left)
   note deq = degree_unique[OF eq]
   {assume p: "poly p = poly []"
     with eq have eq': "poly ([a,1] %^(Suc n) *** p) = poly []"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/List.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -3205,11 +3205,11 @@
 
 lemma (in monoid_add) listsum_triv:
   "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
-  by (induct xs) (simp_all add: left_distrib)
+  by (induct xs) (simp_all add: distrib_right)
 
 lemma (in monoid_add) listsum_0 [simp]:
   "(\<Sum>x\<leftarrow>xs. 0) = 0"
-  by (induct xs) (simp_all add: left_distrib)
+  by (induct xs) (simp_all add: distrib_right)
 
 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
 lemma (in ab_group_add) uminus_listsum_map:
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Log.thy
--- a/src/HOL/Log.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Log.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -34,7 +34,7 @@
 
 lemma powr_mult: 
       "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)"
-by (simp add: powr_def exp_add [symmetric] ln_mult right_distrib)
+by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
 
 lemma powr_gt_zero [simp]: "0 < x powr a"
 by (simp add: powr_def)
@@ -58,7 +58,7 @@
 done
 
 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
-by (simp add: powr_def exp_add [symmetric] left_distrib)
+by (simp add: powr_def exp_add [symmetric] distrib_right)
 
 lemma powr_mult_base:
   "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
@@ -112,7 +112,7 @@
 lemma log_mult: 
      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]  
       ==> log a (x * y) = log a x + log a y"
-by (simp add: log_def ln_mult divide_inverse left_distrib)
+by (simp add: log_def ln_mult divide_inverse distrib_right)
 
 lemma log_eq_div_ln_mult_log: 
      "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
diff -r 1167c1157a5b -r 326f87427719 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/MacLaurin.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -415,7 +415,7 @@
 lemma sin_expansion_lemma:
      "sin (x + real (Suc m) * pi / 2) =
       cos (x + real (m) * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib distrib_right, auto)
 
 lemma Maclaurin_sin_expansion2:
      "\<exists>t. abs t \<le> abs x &
@@ -489,7 +489,7 @@
 
 lemma cos_expansion_lemma:
   "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto)
 
 lemma Maclaurin_cos_expansion:
      "\<exists>t. abs t \<le> abs x &
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Metis_Examples/Binary_Tree.thy
--- a/src/HOL/Metis_Examples/Binary_Tree.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -223,7 +223,7 @@
 apply (induct t1)
  apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
               Suc_eq_plus1)
-by (simp add: left_distrib)
+by (simp add: distrib_right)
 
 lemma (*bt_map_append:*)
      "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -1068,7 +1068,7 @@
           x: "setsum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast
         let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::real^'m"
         show "?P (c*s y1 + y2)"
-        proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib right_distrib cond_application_beta cong del: if_weak_cong)
+        proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left cond_application_beta cong del: if_weak_cong)
           fix j
           have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
               else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -1450,7 +1450,7 @@
     have u2:"u2 \<le> 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
     have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
       apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
-    also have "\<dots> \<le> 1" unfolding right_distrib[symmetric] and as(3) using u1 u2 by auto
+    also have "\<dots> \<le> 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
     finally
     show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
       apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Multivariate_Analysis/L2_Norm.thy
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -165,7 +165,7 @@
   apply (simp add: mult_nonneg_nonneg setsum_nonneg)
   apply (simp add: power2_sum)
   apply (simp add: power_mult_distrib)
-  apply (simp add: right_distrib left_distrib)
+  apply (simp add: distrib_left distrib_right)
   apply (rule ord_le_eq_trans)
   apply (rule setL2_mult_ineq_lemma)
   apply simp
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -1456,7 +1456,7 @@
           by (auto simp add: norm_minus_commute)
         also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
           unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
-          unfolding left_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
+          unfolding distrib_right using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
         also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
         finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using `d>0` by auto
 
@@ -1583,7 +1583,7 @@
         by (auto simp add: algebra_simps)
       also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
         using ** by auto
-      also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm)
+      also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: distrib_right dist_norm)
       finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
       thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
     qed  }
diff -r 1167c1157a5b -r 326f87427719 src/HOL/NSA/CLim.thy
--- a/src/HOL/NSA/CLim.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/NSA/CLim.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -140,7 +140,7 @@
      "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
 apply (induct n)
 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
-apply (auto simp add: left_distrib real_of_nat_Suc)
+apply (auto simp add: distrib_right real_of_nat_Suc)
 apply (case_tac "n")
 apply (auto simp add: mult_ac add_commute)
 done
diff -r 1167c1157a5b -r 326f87427719 src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/NSA/HDeriv.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -209,7 +209,7 @@
 apply (drule_tac
      approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
 apply (auto intro!: approx_add_mono1
-            simp add: left_distrib right_distrib mult_commute add_assoc)
+            simp add: distrib_right distrib_left mult_commute add_assoc)
 apply (rule_tac b1 = "star_of Db * star_of (f x)"
          in add_commute [THEN subst])
 apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
@@ -357,7 +357,7 @@
             del: inverse_mult_distrib inverse_minus_eq
                  minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
-apply (simp (no_asm_simp) add: mult_assoc [symmetric] left_distrib
+apply (simp (no_asm_simp) add: mult_assoc [symmetric] distrib_right
             del: minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (rule_tac y = "inverse (- (star_of x * star_of x))" in approx_trans)
 apply (rule inverse_add_Infinitesimal_approx2)
@@ -451,7 +451,7 @@
 apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
 apply assumption
 apply (simp add: times_divide_eq_right [symmetric])
-apply (auto simp add: left_distrib)
+apply (auto simp add: distrib_right)
 done
 
 lemma increment_thm2:
@@ -464,7 +464,7 @@
 lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
       ==> increment f x h \<approx> 0"
 apply (drule increment_thm2,
-       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
+       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: distrib_right [symmetric] mem_infmal_iff [symmetric])
 apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
 done
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -404,7 +404,7 @@
 
 lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
 apply (induct n)
-apply (auto simp add: left_distrib)
+apply (auto simp add: distrib_right)
 apply (cut_tac n = n in two_hrealpow_ge_one, arith)
 done
 
@@ -417,7 +417,7 @@
 lemma hrealpow_sum_square_expand:
      "(x + (y::hypreal)) ^ Suc (Suc 0) =
       x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
-by (simp add: right_distrib left_distrib)
+by (simp add: distrib_left distrib_right)
 
 lemma power_hypreal_of_real_numeral:
      "(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -547,7 +547,7 @@
    "!!a. hcis (hypreal_of_nat (Suc n) * a) =
      hcis a * hcis (hypreal_of_nat n * a)"
 apply transfer
-apply (simp add: left_distrib cis_mult)
+apply (simp add: distrib_right cis_mult)
 done
 
 lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
@@ -559,7 +559,7 @@
 lemma hcis_hypreal_of_hypnat_Suc_mult:
      "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
       hcis a * hcis (hypreal_of_hypnat n * a)"
-by transfer (simp add: left_distrib cis_mult)
+by transfer (simp add: distrib_right cis_mult)
 
 lemma NSDeMoivre_ext:
   "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -828,8 +828,8 @@
 
 instance star :: (semiring) semiring
 apply (intro_classes)
-apply (transfer, rule left_distrib)
-apply (transfer, rule right_distrib)
+apply (transfer, rule distrib_right)
+apply (transfer, rule distrib_left)
 done
 
 instance star :: (semiring_0) semiring_0 
@@ -838,7 +838,7 @@
 instance star :: (semiring_0_cancel) semiring_0_cancel ..
 
 instance star :: (comm_semiring) comm_semiring 
-by (intro_classes, transfer, rule left_distrib)
+by (intro_classes, transfer, rule distrib_right)
 
 instance star :: (comm_semiring_0) comm_semiring_0 ..
 instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Nat.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -312,7 +312,7 @@
   by (rule mult_commute)
 
 lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
-  by (rule right_distrib)
+  by (rule distrib_left)
 
 lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   by (induct m) auto
@@ -1342,7 +1342,7 @@
   by (induct m) (simp_all add: add_ac)
 
 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
-  by (induct m) (simp_all add: add_ac left_distrib)
+  by (induct m) (simp_all add: add_ac distrib_right)
 
 primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   "of_nat_aux inc 0 i = i"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/NthRoot.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -598,7 +598,7 @@
   "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
 apply (rule power2_le_imp_le, simp)
 apply (simp add: power2_sum)
-apply (simp only: mult_assoc right_distrib [symmetric])
+apply (simp only: mult_assoc distrib_left [symmetric])
 apply (rule mult_left_mono)
 apply (rule power2_le_imp_le)
 apply (simp add: power2_sum power_mult_distrib)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Num.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -138,7 +138,7 @@
   "Bit1 m * Bit0 n = Bit0 (Bit1 m * n)"
   "Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))"
   by (simp_all add: num_eq_iff nat_of_num_add
-    nat_of_num_mult left_distrib right_distrib)
+    nat_of_num_mult distrib_right distrib_left)
 
 lemma eq_num_simps:
   "One = One \<longleftrightarrow> True"
@@ -510,7 +510,7 @@
 lemma numeral_mult: "numeral (m * n) = numeral m * numeral n"
   apply (induct n rule: num_induct)
   apply (simp add: numeral_One)
-  apply (simp add: mult_inc numeral_inc numeral_add right_distrib)
+  apply (simp add: mult_inc numeral_inc numeral_add distrib_left)
   done
 
 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)"
@@ -532,10 +532,10 @@
     simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
 
 lemma mult_2: "2 * z = z + z"
-  unfolding one_add_one [symmetric] left_distrib by simp
+  unfolding one_add_one [symmetric] distrib_right by simp
 
 lemma mult_2_right: "z * 2 = z + z"
-  unfolding one_add_one [symmetric] right_distrib by simp
+  unfolding one_add_one [symmetric] distrib_left by simp
 
 end
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -205,7 +205,7 @@
   also note two
   also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
     apply (subst fact_plus_one_nat)
-    apply (subst left_distrib [symmetric])
+    apply (subst distrib_right [symmetric])
     apply simp
     done
   finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) = 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Old_Number_Theory/EvenOdd.thy
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -85,7 +85,7 @@
 
 lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
   apply (auto simp add: zEven_def)
-  apply (auto simp only: right_distrib [symmetric])
+  apply (auto simp only: distrib_left [symmetric])
   done
 
 lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
@@ -113,9 +113,9 @@
   done
 
 lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd"
-  apply (auto simp add: zOdd_def left_distrib right_distrib)
+  apply (auto simp add: zOdd_def distrib_right distrib_left)
   apply (rule_tac x = "2 * ka * k + ka + k" in exI)
-  apply (auto simp add: left_distrib)
+  apply (auto simp add: distrib_right)
   done
 
 lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Old_Number_Theory/Finite2.thy
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -38,18 +38,18 @@
 
 lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
   apply (induct set: finite)
-  apply (auto simp add: left_distrib right_distrib)
+  apply (auto simp add: distrib_right distrib_left)
   done
 
 lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
     int(c) * int(card X)"
   apply (induct set: finite)
-  apply (auto simp add: right_distrib)
+  apply (auto simp add: distrib_left)
   done
 
 lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
     c * setsum f A"
-  by (induct set: finite) (auto simp add: right_distrib)
+  by (induct set: finite) (auto simp add: distrib_left)
 
 
 subsection {* Cardinality of explicit finite sets *}
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -341,7 +341,7 @@
     apply (elim zcong_trans)
     by (simp only: zcong_refl)
   also have "y * a + ya * a = a * (y + ya)"
-    by (simp add: right_distrib mult_commute)
+    by (simp add: distrib_left mult_commute)
   finally have "[a * (y + ya) = 0] (mod p)" .
   with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
     p_a_relprime
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -341,7 +341,7 @@
 lemma xzgcda_linear_aux1:
   "(a - r * b) * m + (c - r * d) * (n::int) =
    (a * m + c * n) - r * (b * m + d * n)"
-  by (simp add: left_diff_distrib right_distrib mult_assoc)
+  by (simp add: left_diff_distrib distrib_left mult_assoc)
 
 lemma xzgcda_linear_aux2:
   "r' = s' * m + t' * n ==> r = s * m + t * n
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -161,7 +161,7 @@
     and q12': "y + n*q1' = y'+n*q2'" unfolding nat_mod by blast+
   from th[OF q12 q12' yx yx']
   have "(x - y) + n*(q1 + q2') = (x' - y') + n*(q2 + q1')"
-    by (simp add: right_distrib)
+    by (simp add: distrib_left)
   thus ?thesis unfolding nat_mod by blast
 qed
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Presburger.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -54,7 +54,7 @@
   "(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
   "\<forall>x k. F = F"
 apply (auto elim!: dvdE simp add: algebra_simps)
-unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
+unfolding mult_assoc [symmetric] distrib_right [symmetric] left_diff_distrib [symmetric]
 unfolding dvd_def mult_commute [of d] 
 by auto
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -107,7 +107,7 @@
   "n < m \<longleftrightarrow> int_of n < int_of m"
 
 instance proof
-qed (auto simp add: code_int left_distrib zmult_zless_mono2)
+qed (auto simp add: code_int distrib_right zmult_zless_mono2)
 
 end
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -208,7 +208,7 @@
   apply(induct "k")
   apply(simp)
   apply(case_tac "k = 0")
-  apply(simp_all add: left_distrib add_strict_mono)
+  apply(simp_all add: distrib_right add_strict_mono)
   done
 
 lemma zero_le_imp_eq_int_raw:
@@ -248,8 +248,8 @@
 qed
 
 lemmas int_distrib =
-  left_distrib [of z1 z2 w]
-  right_distrib [of w z1 z2]
+  distrib_right [of z1 z2 w]
+  distrib_left [of w z1 z2]
   left_diff_distrib [of z1 z2 w]
   right_diff_distrib [of w z1 z2]
   minus_add_distrib[of z1 z2]
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -128,7 +128,7 @@
   show "1 * a = a"
     by partiality_descending auto
   show "a + b + c = a + (b + c)"
-    by partiality_descending (auto simp add: mult_commute right_distrib)
+    by partiality_descending (auto simp add: mult_commute distrib_left)
   show "a + b = b + a"
     by partiality_descending auto
   show "0 + a = a"
@@ -138,7 +138,7 @@
   show "a - b = a + - b"
     by (simp add: minus_rat_def)
   show "(a + b) * c = a * c + b * c"
-    by partiality_descending (auto simp add: mult_commute right_distrib)
+    by partiality_descending (auto simp add: mult_commute distrib_left)
   show "(0 :: rat) \<noteq> (1 :: rat)"
     by partiality_descending auto
 qed
diff -r 1167c1157a5b -r 326f87427719 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/RComplete.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -447,7 +447,7 @@
     done
   thus "x / real y < real (natfloor x div y) + 1"
     using assms
-    by (simp add: divide_less_eq natfloor_less_iff left_distrib)
+    by (simp add: divide_less_eq natfloor_less_iff distrib_right)
 qed
 
 lemma le_mult_natfloor:
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Rat.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -123,7 +123,7 @@
 
 lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
   is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
-  by (clarsimp, simp add: left_distrib, simp add: mult_ac)
+  by (clarsimp, simp add: distrib_right, simp add: mult_ac)
 
 lemma add_rat [simp]:
   assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -616,8 +616,8 @@
     (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
   #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
       @{thm True_implies_equals},
-      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm right_distrib},
-      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm right_distrib},
+      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
+      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left},
       @{thm divide_1}, @{thm divide_zero_left},
       @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
       @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
diff -r 1167c1157a5b -r 326f87427719 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/RealDef.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -494,7 +494,7 @@
   show "1 * a = a"
     by transfer (simp add: mult_ac realrel_def)
   show "(a + b) * c = a * c + b * c"
-    by transfer (simp add: left_distrib realrel_def)
+    by transfer (simp add: distrib_right realrel_def)
   show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
     by transfer (simp add: realrel_def)
   show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
diff -r 1167c1157a5b -r 326f87427719 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/RealVector.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -1081,8 +1081,8 @@
 lemma bounded_bilinear_mult:
   "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
 apply (rule bounded_bilinear.intro)
-apply (rule left_distrib)
-apply (rule right_distrib)
+apply (rule distrib_right)
+apply (rule distrib_left)
 apply (rule mult_scaleR_left)
 apply (rule mult_scaleR_right)
 apply (rule_tac x="1" in exI)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -14,14 +14,14 @@
 begin
 
 class semiring = ab_semigroup_add + semigroup_mult +
-  assumes left_distrib[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
-  assumes right_distrib[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
+  assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
+  assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
 begin
 
 text{*For the @{text combine_numerals} simproc*}
 lemma combine_common_factor:
   "a * e + (b * e + c) = (a + b) * e + c"
-by (simp add: left_distrib add_ac)
+by (simp add: distrib_right add_ac)
 
 end
 
@@ -37,11 +37,11 @@
 subclass semiring_0
 proof
   fix a :: 'a
-  have "0 * a + 0 * a = 0 * a + 0" by (simp add: left_distrib [symmetric])
+  have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric])
   thus "0 * a = 0" by (simp only: add_left_cancel)
 next
   fix a :: 'a
-  have "a * 0 + a * 0 = a * 0 + 0" by (simp add: right_distrib [symmetric])
+  have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric])
   thus "a * 0 = 0" by (simp only: add_left_cancel)
 qed
 
@@ -177,7 +177,7 @@
 proof -
   from `a dvd b` obtain b' where "b = a * b'" ..
   moreover from `a dvd c` obtain c' where "c = a * c'" ..
-  ultimately have "b + c = a * (b' + c')" by (simp add: right_distrib)
+  ultimately have "b + c = a * (b' + c')" by (simp add: distrib_left)
   then show ?thesis ..
 qed
 
@@ -227,10 +227,10 @@
 text {* Distribution rules *}
 
 lemma minus_mult_left: "- (a * b) = - a * b"
-by (rule minus_unique) (simp add: left_distrib [symmetric]) 
+by (rule minus_unique) (simp add: distrib_right [symmetric]) 
 
 lemma minus_mult_right: "- (a * b) = a * - b"
-by (rule minus_unique) (simp add: right_distrib [symmetric]) 
+by (rule minus_unique) (simp add: distrib_left [symmetric]) 
 
 text{*Extract signs from products*}
 lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
@@ -243,13 +243,13 @@
 by simp
 
 lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"
-by (simp add: right_distrib diff_minus)
+by (simp add: distrib_left diff_minus)
 
 lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
-by (simp add: left_distrib diff_minus)
+by (simp add: distrib_right diff_minus)
 
 lemmas ring_distribs[no_atp] =
-  right_distrib left_distrib left_diff_distrib right_diff_distrib
+  distrib_left distrib_right left_diff_distrib right_diff_distrib
 
 lemma eq_add_iff1:
   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
@@ -262,7 +262,7 @@
 end
 
 lemmas ring_distribs[no_atp] =
-  right_distrib left_distrib left_diff_distrib right_diff_distrib
+  distrib_left distrib_right left_diff_distrib right_diff_distrib
 
 class comm_ring = comm_semiring + ab_group_add
 begin
@@ -506,7 +506,7 @@
 proof-
   from assms have "u * x + v * y \<le> u * a + v * a"
     by (simp add: add_mono mult_left_mono)
-  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
+  thus ?thesis using assms unfolding distrib_right[symmetric] by simp
 qed
 
 end
@@ -640,7 +640,7 @@
   from assms have "u * x + v * y < u * a + v * a"
     by (cases "u = 0")
        (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
-  thus ?thesis using assms unfolding left_distrib[symmetric] by simp
+  thus ?thesis using assms unfolding distrib_right[symmetric] by simp
 qed
 
 end
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Transcendental.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -35,7 +35,7 @@
 apply (simp del: setsum_op_ivl_Suc)
 apply (subst setsum_op_ivl_Suc)
 apply (subst lemma_realpow_diff_sumr)
-apply (simp add: right_distrib del: setsum_op_ivl_Suc)
+apply (simp add: distrib_left del: setsum_op_ivl_Suc)
 apply (subst mult_left_commute [of "x - y"])
 apply (erule subst)
 apply (simp add: algebra_simps)
@@ -922,7 +922,7 @@
     by (simp only: Suc)
   also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
                 + y * (\<Sum>i=0..n. S x i * S y (n-i))"
-    by (rule left_distrib)
+    by (rule distrib_right)
   also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
                 + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
     by (simp only: setsum_right_distrib mult_ac)
@@ -1001,7 +1001,7 @@
 
 lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
 apply (induct "n")
-apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
+apply (auto simp add: real_of_nat_Suc distrib_left exp_add mult_commute)
 done
 
 text {* Strict monotonicity of exponential. *}
@@ -1626,7 +1626,7 @@
 
 lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
 apply (induct "n")
-apply (auto simp add: real_of_nat_Suc left_distrib)
+apply (auto simp add: real_of_nat_Suc distrib_right)
 done
 
 lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
@@ -1638,7 +1638,7 @@
 
 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
 apply (induct "n")
-apply (auto simp add: real_of_nat_Suc left_distrib)
+apply (auto simp add: real_of_nat_Suc distrib_right)
 done
 
 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
@@ -1784,7 +1784,7 @@
       \<exists>n::nat. even n & x = real n * (pi/2)"
 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  apply (clarify, rule_tac x = "n - 1" in exI)
- apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
+ apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
 apply (rule cos_zero_lemma)
 apply (simp_all add: cos_add)
 done
@@ -1799,7 +1799,7 @@
 apply (drule cos_zero_lemma, assumption+)
 apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
 apply (force simp add: minus_equation_iff [of x])
-apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
+apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
 apply (auto simp add: cos_add)
 done
 
@@ -2029,7 +2029,7 @@
 lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
 proof (induct n arbitrary: x)
   case (Suc n)
-  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
+  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
   show ?case unfolding split_pi_off using Suc by auto
 qed auto
 
@@ -2212,7 +2212,7 @@
   show "0 \<le> cos (arctan x)"
     by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
   have "(cos (arctan x))\<twosuperior> * (1 + (tan (arctan x))\<twosuperior>) = 1"
-    unfolding tan_def by (simp add: right_distrib power_divide)
+    unfolding tan_def by (simp add: distrib_left power_divide)
   thus "(cos (arctan x))\<twosuperior> = (1 / sqrt (1 + x\<twosuperior>))\<twosuperior>"
     using `0 < 1 + x\<twosuperior>` by (simp add: power_divide eq_divide_eq)
 qed
@@ -2226,7 +2226,7 @@
 apply (rule power_inverse [THEN subst])
 apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
 apply (auto dest: field_power_not_zero
-        simp add: power_mult_distrib left_distrib power_divide tan_def
+        simp add: power_mult_distrib distrib_right power_divide tan_def
                   mult_assoc power_inverse [symmetric])
 done
 
@@ -2397,7 +2397,7 @@
   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
     by (auto simp add: algebra_simps sin_add)
   thus ?thesis
-    by (simp add: real_of_nat_Suc left_distrib add_divide_distrib
+    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
                   mult_commute [of pi])
 qed
 
@@ -2418,7 +2418,7 @@
 done
 
 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
+by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
 
 lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
   by (auto intro!: DERIV_intros)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -301,7 +301,7 @@
   apply assumption
   done
 
-lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified]
+lemmas less_le_mult = less_le_mult' [simplified distrib_right, simplified]
 
 lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, 
   simplified left_diff_distrib]
diff -r 1167c1157a5b -r 326f87427719 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -308,7 +308,7 @@
     using Cons
     apply (simp add: trans [OF of_bl_append add_commute]
                      rbl_mul_simps rbl_word_plus'
-                     Cons.hyps left_distrib mult_bit
+                     Cons.hyps distrib_right mult_bit
                      shiftl rbl_shiftl)
     apply (simp add: takefill_alt word_size rev_map take_rbl_plus
                      min_def)
diff -r 1167c1157a5b -r 326f87427719 src/HOL/ex/BT.thy
--- a/src/HOL/ex/BT.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/ex/BT.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -107,7 +107,7 @@
 
 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
   apply (induct t)
-   apply (simp_all add: left_distrib)
+   apply (simp_all add: distrib_right)
   done
 
 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
@@ -148,7 +148,7 @@
 lemma n_leaves_append [simp]:
      "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
   apply (induct t1)
-   apply (simp_all add: left_distrib)
+   apply (simp_all add: distrib_right)
   done
 
 lemma bt_map_append:
diff -r 1167c1157a5b -r 326f87427719 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -285,7 +285,7 @@
   show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
   proof (intro bexI)
     show "z = x*?f + y*?f"
-      by (simp add: left_distrib [symmetric] divide_inverse mult_ac
+      by (simp add: distrib_right [symmetric] divide_inverse mult_ac
           order_less_imp_not_eq2)
   next
     show "y * ?f \<in> B"
@@ -534,7 +534,7 @@
 lemma distrib_subset1:
      "Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
-apply (force simp add: right_distrib)
+apply (force simp add: distrib_left)
 done
 
 lemma preal_add_mult_distrib_mean:
@@ -555,13 +555,13 @@
   proof (cases rule: linorder_le_cases)
     assume "a \<le> b"
     hence "?c \<le> b"
-      by (simp add: pos_divide_le_eq right_distrib mult_right_mono
+      by (simp add: pos_divide_le_eq distrib_left mult_right_mono
                     order_less_imp_le)
     thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
   next
     assume "b \<le> a"
     hence "?c \<le> a"
-      by (simp add: pos_divide_le_eq right_distrib mult_right_mono
+      by (simp add: pos_divide_le_eq distrib_left mult_right_mono
                     order_less_imp_le)
     thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
   qed
@@ -1333,7 +1333,7 @@
           x * x1 + y * y1 + (x * y2 + y * x2) =
           x * x2 + y * y2 + (x * y1 + y * x1)"
 apply (simp add: add_left_commute add_assoc [symmetric])
-apply (simp add: add_assoc right_distrib [symmetric])
+apply (simp add: add_assoc distrib_left [symmetric])
 apply (simp add: add_commute)
 done
 
@@ -1543,7 +1543,7 @@
 apply (rule real_sum_gt_zero_less)
 apply (drule real_less_sum_gt_zero [of x y])
 apply (drule real_mult_order, assumption)
-apply (simp add: right_distrib)
+apply (simp add: distrib_left)
 done
 
 instantiation real :: distrib_lattice
@@ -1986,7 +1986,7 @@
     from t_is_Lub have "x * of_nat (Suc n) \<le> t"
       by (simp add: isLubD2)
     hence  "x * (of_nat n) + x \<le> t"
-      by (simp add: right_distrib)
+      by (simp add: distrib_left)
     thus  "x * (of_nat n) \<le> t + - x" by arith
   qed
 
diff -r 1167c1157a5b -r 326f87427719 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -521,9 +521,9 @@
                     = (f z - f x) / (z - x) - f' x")
  apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
 apply (subst mult_commute)
-apply (simp add: left_distrib diff_minus)
+apply (simp add: distrib_right diff_minus)
 apply (simp add: mult_assoc divide_inverse)
-apply (simp add: left_distrib)
+apply (simp add: distrib_right)
 done
 
 lemma lemma_straddle:
diff -r 1167c1157a5b -r 326f87427719 src/HOL/ex/Numeral_Representation.thy
--- a/src/HOL/ex/Numeral_Representation.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/ex/Numeral_Representation.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -153,7 +153,7 @@
   "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
   "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
   by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
-                    left_distrib right_distrib)
+                    distrib_right distrib_left)
 
 lemma less_eq_num_code [numeral, simp, code]:
   "One \<le> n \<longleftrightarrow> True"
@@ -243,7 +243,7 @@
   by (induct n rule: num_induct) (simp_all add: add_One add_inc of_num_inc add_ac)
 
 lemma of_num_mult: "of_num (m * n) = of_num m * of_num n"
-  by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc right_distrib)
+  by (induct n rule: num_induct) (simp_all add: mult_One mult_inc of_num_add of_num_inc distrib_left)
 
 declare of_num.simps [simp del]
 
@@ -792,7 +792,7 @@
 
 lemma mult_of_num_commute: "x * of_num n = of_num n * x"
 by (induct n)
-  (simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right)
+  (simp_all only: of_num.simps distrib_right distrib_left mult_1_left mult_1_right)
 
 definition
   "commutes_with a b \<longleftrightarrow> a * b = b * a"