# HG changeset patch
# User haftmann
# Date 1404550913 -7200
# Node ID bdc2c6b40bf2407400052536d89f533df9100709
# Parent  55b2afc5ddfcd7d34f0ad2dac79977ca01b41f78
prefer ac_simps collections over separate name bindings for add and mult

diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/Doc/How_to_Prove_it/How_to_Prove_it.thy
--- a/src/Doc/How_to_Prove_it/How_to_Prove_it.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/Doc/How_to_Prove_it/How_to_Prove_it.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -113,10 +113,10 @@
 
 Because @{thm[source]algebra_simps} multiplies out, terms can explode.
 If one merely wants to bring sums or products into a canonical order
-it suffices to rewrite with @{thm [source] add_ac} or @{thm [source] mult_ac}: *}
+it suffices to rewrite with @{thm [source] ac_simps}: *}
 
 lemma fixes f :: "int \<Rightarrow> int" shows "f(x*y*z) - f(z*x*y) = 0"
-by(simp add: mult_ac)
+by(simp add: ac_simps)
 
 text{* The lemmas @{thm[source]algebra_simps} take care of addition, subtraction
 and multiplication (algebraic structures up to rings) but ignore division (fields).
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/Doc/Tutorial/Types/Numbers.thy
--- a/src/Doc/Tutorial/Types/Numbers.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/Doc/Tutorial/Types/Numbers.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -40,14 +40,14 @@
 @{thm[display] add.left_commute[no_vars]}
 \rulename{add.left_commute}
 
-these form add_ac; similarly there is mult_ac
+these form ac_simps; similarly there is ac_simps
 *}
 
 lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 *};
-apply (simp add: add_ac mult_ac)
+apply (simp add: ac_simps ac_simps)
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 *};
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/Doc/Tutorial/document/numerics.tex
--- a/src/Doc/Tutorial/document/numerics.tex	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/Doc/Tutorial/document/numerics.tex	Sat Jul 05 11:01:53 2014 +0200
@@ -447,9 +447,9 @@
 a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
 \rulename{add.left_commute}
 \end{isabelle}
-The name \isa{add_ac}\index{*add_ac (theorems)} 
+The name \isa{ac_simps}\index{*ac_simps (theorems)} 
 refers to the list of all three theorems; similarly
-there is \isa{mult_ac}.\index{*mult_ac (theorems)} 
+there is \isa{ac_simps}.\index{*ac_simps (theorems)} 
 They are all proved for semirings and therefore hold for all numeric types.
 
 Here is an example of the sorting effect.  Start
@@ -459,9 +459,9 @@
 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
 \end{isabelle}
 %
-Simplify using  \isa{add_ac} and \isa{mult_ac}.
+Simplify using  \isa{ac_simps} and \isa{ac_simps}.
 \begin{isabelle}
-\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
+\isacommand{apply}\ (simp\ add:\ ac_simps\ ac_simps)
 \end{isabelle}
 %
 Here is the resulting subgoal.
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -290,7 +290,7 @@
   apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
   apply (rule, clarify)
   apply (simp add: dvd_def)
-  apply (simp add: dvd_def mult_ac)
+  apply (simp add: dvd_def ac_simps)
   done
 
 lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1695,7 +1695,7 @@
   also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
     by (simp only: dvd_minus_iff)
   also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
-    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
+    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
       (simp add: algebra_simps)
   also have "\<dots> = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
@@ -1709,7 +1709,7 @@
   also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
     by (simp only: dvd_minus_iff)
   also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
-    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
+    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
       (simp add: algebra_simps)
   also have "\<dots> \<longleftrightarrow> Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1059,7 +1059,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     hence "real c * x + ?e \<noteq> 0" by simp
     with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -1076,7 +1076,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     hence "real c * x + ?e \<noteq> 0" by simp
     with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -1093,7 +1093,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     with xz have "?P ?z x (Lt (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]  by simp }
@@ -1109,7 +1109,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     with xz have "?P ?z x (Le (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1125,7 +1125,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     with xz have "?P ?z x (Gt (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1141,7 +1141,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     with xz have "?P ?z x (Ge (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1167,7 +1167,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     hence "real c * x + ?e \<noteq> 0" by simp
     with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -1184,7 +1184,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     hence "real c * x + ?e \<noteq> 0" by simp
     with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -1201,7 +1201,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     with xz have "?P ?z x (Lt (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1217,7 +1217,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     with xz have "?P ?z x (Le (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1233,7 +1233,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     with xz have "?P ?z x (Gt (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1249,7 +1249,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     with xz have "?P ?z x (Ge (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]   by simp }
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1542,10 +1542,10 @@
   have th': "(real ?nt)*(real x) = real (?nt * x)" by simp
   have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp
   also have "\<dots> = real (floor ((real ?nt)* real(x) + ?I x ?at))" by simp
-  also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: add_ac)
+  also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: ac_simps)
   also have "\<dots> = real (floor (?I x ?at) + (?nt* x))" 
     using floor_add[where x="?I x ?at" and a="?nt* x"] by simp 
-  also have "\<dots> = real (?nt)*(real x) + real (floor (?I x ?at))" by (simp add: add_ac)
+  also have "\<dots> = real (?nt)*(real x) + real (floor (?I x ?at))" by (simp add: ac_simps)
   finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp
   with na show ?case by simp
 qed
@@ -1733,7 +1733,7 @@
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
-    also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
+    also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def ac_simps, arith)
     finally have ?case using l by simp}
   ultimately show ?case by blast
 next
@@ -1758,7 +1758,7 @@
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
-    also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
+    also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def ac_simps, arith)
     finally have ?case using l by simp}
   ultimately show ?case by blast
 next
@@ -1783,7 +1783,7 @@
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
-    also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
+    also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def ac_simps, arith)
     finally have ?case using l by simp}
   ultimately show ?case by blast
 next
@@ -1808,7 +1808,7 @@
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
       by (simp add: nb Let_def split_def isint_Floor isint_neg)
     have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
-    also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
+    also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def ac_simps, arith)
     finally have ?case using l by simp}
   ultimately show ?case by blast
 next
@@ -1886,10 +1886,10 @@
       by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
     also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 
        (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))" 
-      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
+      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (Dvd j a)))" using cp cnz jnz  
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]  
-        del: real_of_int_mult) (auto simp add: add_ac)
+        del: real_of_int_mult) (auto simp add: ac_simps)
     finally have ?case using l jnz  by simp }
   moreover
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
@@ -1900,11 +1900,11 @@
       by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
     also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 
        (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))" 
-      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
+      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (Dvd j a)))" using cn cnz jnz
       using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric]
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]  
-        del: real_of_int_mult) (auto simp add: add_ac)
+        del: real_of_int_mult) (auto simp add: ac_simps)
     finally have ?case using l jnz by blast }
   ultimately show ?case by blast
 next
@@ -1932,10 +1932,10 @@
       by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
     also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 
        (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))" 
-      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
+      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (NDvd j a)))" using cp cnz jnz  
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]  
-        del: real_of_int_mult) (auto simp add: add_ac)
+        del: real_of_int_mult) (auto simp add: ac_simps)
     finally have ?case using l jnz  by simp }
   moreover
   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (NDvd j a))" 
@@ -1946,11 +1946,11 @@
       by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
     also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 
        (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))" 
-      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
+      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
     also have "\<dots> = (?I (?l (NDvd j a)))" using cn cnz jnz
       using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric]
       by (simp add: Let_def split_def int_rdvd_iff[symmetric]  
-        del: real_of_int_mult) (auto simp add: add_ac)
+        del: real_of_int_mult) (auto simp add: ac_simps)
     finally have ?case using l jnz by blast }
   ultimately show ?case by blast
 qed auto
@@ -4159,7 +4159,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     hence "real c * x + ?e \<noteq> 0" by simp
     with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -4176,7 +4176,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     hence "real c * x + ?e \<noteq> 0" by simp
     with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -4193,7 +4193,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     with xz have "?P ?z x (Lt (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]  by simp }
@@ -4209,7 +4209,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     with xz have "?P ?z x (Le (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4225,7 +4225,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     with xz have "?P ?z x (Gt (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4241,7 +4241,7 @@
   {fix x
     assume xz: "x < ?z"
     hence "(real c * x < - ?e)" 
-      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
+      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     hence "real c * x + ?e < 0" by arith
     with xz have "?P ?z x (Ge (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4267,7 +4267,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     hence "real c * x + ?e \<noteq> 0" by simp
     with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -4284,7 +4284,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     hence "real c * x + ?e \<noteq> 0" by simp
     with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -4301,7 +4301,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     with xz have "?P ?z x (Lt (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4317,7 +4317,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     with xz have "?P ?z x (Le (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4333,7 +4333,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     with xz have "?P ?z x (Gt (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4349,7 +4349,7 @@
   {fix x
     assume xz: "x > ?z"
     with mult_strict_right_mono [OF xz cp] cp
-    have "(real c * x > - ?e)" by (simp add: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: ac_simps)
     hence "real c * x + ?e > 0" by arith
     with xz have "?P ?z x (Ge (CN 0 c e))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]   by simp }
@@ -4829,9 +4829,9 @@
   shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
 proof-
   have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
-    by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac)
+    by (simp add: myless[of _ "1"] myless[of _ "0"] ac_simps)
   also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
-    by (simp only: exsplit[OF qf] add_ac)
+    by (simp only: exsplit[OF qf] ac_simps)
   also have "\<dots> = (\<exists> x. Ifm (x#bs) p)" 
     by (simp only: real_ex_int_real01[where P="\<lambda> x. Ifm (x#bs) p"])
   finally show ?thesis by simp
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -127,7 +127,7 @@
 lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
   apply (induct a)
   apply (simp, clarify)
-  apply (case_tac b, simp_all add: add_ac)
+  apply (case_tac b, simp_all add: ac_simps)
   done
 
 lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
@@ -152,17 +152,17 @@
 next
   case (Cons a as p2)
   thus ?case
-    by (cases p2) (simp_all  add: add_ac distrib_left)
+    by (cases p2) (simp_all  add: ac_simps 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: distrib_left mult_ac)
+  apply (auto simp add: distrib_left ac_simps)
   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: distrib_left mult_ac)
+  by (induct p) (auto simp add: distrib_left ac_simps)
 
 lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
   apply (simp add: poly_minus_def)
@@ -176,7 +176,7 @@
 next
   case (Cons a as p2)
   thus ?case by (cases as)
-    (simp_all add: poly_cmult poly_add distrib_right distrib_left mult_ac)
+    (simp_all add: poly_cmult poly_add distrib_right distrib_left ac_simps)
 qed
 
 class idom_char_0 = idom + ring_char_0
@@ -505,7 +505,7 @@
   apply (auto simp add: 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)
+  apply (auto simp add: poly_add poly_mult poly_cmult ac_simps)
   done
 
 lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p"
@@ -526,7 +526,7 @@
   apply (rule_tac [2] poly_divides_trans)
   apply (auto simp add: divides_def)
   apply (rule_tac x = p in exI)
-  apply (auto simp add: poly_mult fun_eq mult_ac)
+  apply (auto simp add: poly_mult fun_eq ac_simps)
   done
 
 lemma (in comm_semiring_1) poly_exp_divides:
@@ -550,7 +550,7 @@
 lemma (in comm_ring_1) poly_divides_diff2:
   "p divides r \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides q"
   apply (erule poly_divides_diff)
-  apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
+  apply (auto simp add: poly_add fun_eq poly_mult divides_def ac_simps)
   done
 
 lemma (in semiring_0) poly_divides_zero: "poly p = poly [] \<Longrightarrow> q divides p"
@@ -608,7 +608,7 @@
 
 
 lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
-  by (induct n) (auto simp add: poly_mult mult_ac)
+  by (induct n) (auto simp add: poly_mult ac_simps)
 
 lemma (in comm_semiring_1) divides_left_mult:
   assumes d:"(p***q) divides r" shows "p divides r \<and> q divides r"
@@ -616,7 +616,7 @@
   from d obtain t where r:"poly r = poly (p***q *** t)"
     unfolding divides_def by blast
   hence "poly r = poly (p *** (q *** t))"
-    "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult mult_ac)
+    "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult ac_simps)
   thus ?thesis unfolding divides_def by blast
 qed
 
@@ -742,7 +742,7 @@
   apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
   apply (rule_tac x = q in exI, safe)
   apply (drule_tac x = qa in spec)
-  apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
+  apply (auto simp add: poly_mult fun_eq poly_exp ac_simps simp del: pmult_Cons)
   done
 
 text{*Important composition properties of orders.*}
@@ -755,7 +755,7 @@
   apply safe
   apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
   apply (rule_tac x = "qa *** qaa" in exI)
-  apply (simp add: poly_mult mult_ac del: pmult_Cons)
+  apply (simp add: poly_mult ac_simps del: pmult_Cons)
   apply (drule_tac a = a in order_decomp)+
   apply safe
   apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
@@ -766,7 +766,7 @@
   apply (drule poly_mult_left_cancel [THEN iffD1], force)
   apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
   apply (drule poly_mult_left_cancel [THEN iffD1], force)
-  apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
+  apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons)
   done
 
 lemma (in idom_char_0) order_mult:
@@ -779,7 +779,7 @@
   apply safe
   apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
   apply (rule_tac x = "pmult qa qaa" in exI)
-  apply (simp add: poly_mult mult_ac del: pmult_Cons)
+  apply (simp add: poly_mult ac_simps del: pmult_Cons)
   apply (drule_tac a = a in order_decomp)+
   apply safe
   apply (subgoal_tac "[uminus a, one] divides pmult qa qaa")
@@ -794,7 +794,7 @@
     poly (pmult (pexp [uminus a, one] (order a q))
       (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))")
   apply (drule poly_mult_left_cancel [THEN iffD1], force)
-  apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
+  apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons)
   done
 
 lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] \<Longrightarrow> poly p a = 0 \<longleftrightarrow> order a p \<noteq> 0"
@@ -988,7 +988,7 @@
   have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))"
     apply (rule ext)
     apply (simp add: poly_mult poly_add poly_cmult)
-    apply (simp add: mult_ac add_ac distrib_left)
+    apply (simp add: ac_simps ac_simps distrib_left)
     done
   note deq = degree_unique[OF eq]
   show ?case
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Jul 05 11:01:53 2014 +0200
@@ -53,7 +53,7 @@
           div_by_0 mod_by_0 div_0 mod_0
           div_by_1 mod_by_1 div_1 mod_1
           Suc_eq_plus1}
-      addsimps @{thms add_ac}
+      addsimps @{thms ac_simps}
       addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     val simpset0 =
       put_simpset HOL_basic_ss ctxt
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Jul 05 11:01:53 2014 +0200
@@ -19,8 +19,7 @@
   val nat_arith = [@{thm diff_nat_numeral}];
 
   val comp_arith = [@{thm "Let_def"}, @{thm "if_False"}, @{thm "if_True"}, @{thm "add_0"},
-                 @{thm "add_Suc"}, @{thm add_numeral_left}, @{thm mult_numeral_left(1)},
-                 @{thm "Suc_eq_plus1"}] @
+                 @{thm "add_Suc"}, @{thm add_numeral_left}, @{thm mult_numeral_left(1)}] @
                  (map (fn th => th RS sym) [@{thm "numeral_1_eq_1"}])
                  @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} 
   val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 
@@ -81,7 +80,7 @@
                                   @{thm div_0}, @{thm mod_0},
                                   @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
                                   @{thm "Suc_eq_plus1"}]
-                        addsimps @{thms add_ac}
+                        addsimps @{thms add.assoc add.commute add.left_commute}
                         addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     val simpset0 = put_simpset HOL_basic_ss ctxt
       addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Deriv.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -681,7 +681,7 @@
 
 lemma DERIV_cmult_right:
   "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
-  using DERIV_cmult by (force simp add: mult_ac)
+  using DERIV_cmult by (force simp add: ac_simps)
 
 lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
   by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
@@ -717,7 +717,7 @@
 lemma DERIV_inverse_fun:
   "(f has_field_derivative d) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
   ((\<lambda>x. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)"
-  by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
+  by (drule (1) DERIV_inverse') (simp add: ac_simps nonzero_inverse_mult_distrib)
 
 text {* Derivative of quotient *}
 
@@ -1479,7 +1479,7 @@
   ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto
   with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp
   hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp
-  hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac)
+  hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: ac_simps)
 
   with g'cdef f'cdef cint show ?thesis by auto
 qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Divides.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -34,7 +34,7 @@
 
 lemma mod_div_equality': "a mod b + a div b * b = a"
   using mod_div_equality [of a b]
-  by (simp only: add_ac)
+  by (simp only: ac_simps)
 
 lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
   by (simp add: mod_div_equality)
@@ -228,7 +228,7 @@
   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
     by (simp only: mod_div_equality)
   also have "\<dots> = (a mod c + b + a div c * c) mod c"
-    by (simp only: add_ac)
+    by (simp only: ac_simps)
   also have "\<dots> = (a mod c + b) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .
@@ -239,7 +239,7 @@
   have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
     by (simp only: mod_div_equality)
   also have "\<dots> = (a + b mod c + b div c * c) mod c"
-    by (simp only: add_ac)
+    by (simp only: ac_simps)
   also have "\<dots> = (a + b mod c) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis .
@@ -321,7 +321,7 @@
   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
     by (simp only: mod_mult_self1)
   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
-    by (simp only: add_ac mult_ac)
+    by (simp only: ac_simps ac_simps)
   also have "\<dots> = a mod c"
     by (simp only: mod_div_equality)
   finally show ?thesis .
@@ -421,7 +421,7 @@
   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
     by (simp only: mod_div_equality)
   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
-    by (simp only: minus_add_distrib minus_mult_left add_ac)
+    by (simp add: ac_simps)
   also have "\<dots> = (- (a mod b)) mod b"
     by (rule mod_mult_self1)
   finally show ?thesis .
@@ -957,7 +957,7 @@
   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
 
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
-    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
+    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps}))
 )
 *}
 
@@ -1059,7 +1059,7 @@
 lemma divmod_nat_rel_mult2_eq:
   "divmod_nat_rel a b (q, r)
    \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
-by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
+by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
 
 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
@@ -1147,11 +1147,15 @@
 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
 
 (*Loses information, namely we also have r<d provided d is nonzero*)
-lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
-  apply (cut_tac a = m in mod_div_equality)
-  apply (simp only: add_ac)
-  apply (blast intro: sym)
-  done
+lemma mod_eqD:
+  fixes m d r q :: nat
+  assumes "m mod d = r"
+  shows "\<exists>q. m = r + q * d"
+proof -
+  from mod_div_equality obtain q where "q * d + m mod d = m" by blast
+  with assms have "m = r + q * d" by simp
+  then show ?thesis ..
+qed
 
 lemma split_div:
  "P(n div k :: nat) =
@@ -1175,7 +1179,7 @@
         with n j P show "P i" by simp
       next
         assume "i \<noteq> 0"
-        with not0 n j P show "P i" by(simp add:add_ac)
+        with not0 n j P show "P i" by(simp add:ac_simps)
       qed
     qed
   qed
@@ -1209,7 +1213,7 @@
 next
   assume P: ?lhs
   then have "divmod_nat_rel m n (q, m - n * q)"
-    unfolding divmod_nat_rel_def by (auto simp add: mult_ac)
+    unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
   with divmod_nat_rel_unique divmod_nat_rel [of m n]
   have "(q, m - n * q) = (m div n, m mod n)" by auto
   then show ?rhs by simp
@@ -1239,7 +1243,7 @@
     proof (simp, intro allI impI)
       fix i j
       assume "n = k*i + j" "j < k"
-      thus "P j" using not0 P by(simp add:add_ac mult_ac)
+      thus "P j" using not0 P by(simp add:ac_simps ac_simps)
     qed
   qed
 next
@@ -1417,7 +1421,7 @@
 
   (* Potential use of algebra : Equality modulo n*)
 lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
-by (simp add: mult_ac add_ac)
+by (simp add: ac_simps ac_simps)
 
 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
 proof -
@@ -1614,7 +1618,7 @@
   apply (case_tac "a < b")
   apply simp_all
   apply (erule splitE)
-  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
+  apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
   done
 
 
@@ -1644,7 +1648,7 @@
   apply (case_tac "a + b < (0\<Colon>int)")
   apply simp_all
   apply (erule splitE)
-  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
+  apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
   done
 
 
@@ -1744,7 +1748,7 @@
   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
 
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
-    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms add_ac}))
+    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms ac_simps}))
 )
 *}
 
@@ -2072,7 +2076,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 distrib_left mult_ac)
+by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
 
 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)
@@ -2176,7 +2180,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
+by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
                    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)
 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Fact.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -256,14 +256,10 @@
   apply (induct k rule: int_ge_induct)
   apply (simp add: fact_plus_one_int)
   apply (subst (2) fact_reduce_int)
-  apply (auto simp add: add_ac)
+  apply (auto simp add: ac_simps)
   apply (erule order_less_le_trans)
-  apply (subst mult_le_cancel_right1)
   apply auto
-  apply (subgoal_tac "fact (i + (1 + m)) >= 0")
-  apply force
-  apply (rule fact_ge_zero_int)
-done
+  done
 
 lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
   apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Fields.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -310,7 +310,7 @@
 lemma inverse_add:
   "[| a \<noteq> 0;  b \<noteq> 0 |]
    ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
-by (simp add: division_ring_inverse_add mult_ac)
+by (simp add: division_ring_inverse_add ac_simps)
 
 lemma nonzero_mult_divide_mult_cancel_left [simp]:
 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
@@ -318,7 +318,7 @@
   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
     by (simp add: divide_inverse nonzero_inverse_mult_distrib)
   also have "... =  a * inverse b * (inverse c * c)"
-    by (simp only: mult_ac)
+    by (simp only: ac_simps)
   also have "... =  a * inverse b" by simp
     finally show ?thesis by (simp add: divide_inverse)
 qed
@@ -328,7 +328,7 @@
 by (simp add: mult.commute [of _ c])
 
 lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
-  by (simp add: divide_inverse mult_ac)
+  by (simp add: divide_inverse ac_simps)
 
 text{*It's not obvious whether @{text times_divide_eq} should be
   simprules or not. Their effect is to gather terms into one big
@@ -369,11 +369,11 @@
 
 lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
-using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
+using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: ac_simps)
 
 lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
-using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
+using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
 
 lemma diff_frac_eq:
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
@@ -398,7 +398,7 @@
   "inverse (a * b) = inverse a * inverse b"
 proof cases
   assume "a \<noteq> 0 & b \<noteq> 0" 
-  thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
+  thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps)
 next
   assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
   thus ?thesis by force
@@ -429,7 +429,7 @@
 
 lemma divide_divide_eq_right [simp]:
   "a / (b / c) = (a * c) / b"
-  by (simp add: divide_inverse mult_ac)
+  by (simp add: divide_inverse ac_simps)
 
 lemma divide_divide_eq_left [simp]:
   "(a / b) / c = a / (b * c)"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/GCD.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1225,7 +1225,7 @@
           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
-            by (simp only: diff_mult_distrib2 add.commute mult_ac)
+            by (simp only: diff_mult_distrib2 add.commute ac_simps)
           hence ?thesis using H(1,2)
             apply -
             apply (rule exI[where x=d], simp)
@@ -1312,20 +1312,20 @@
   from pos_k k_m have pos_p: "p > 0" by auto
   from pos_k k_n have pos_q: "q > 0" by auto
   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
-    by (simp add: mult_ac gcd_mult_distrib_nat)
+    by (simp add: ac_simps gcd_mult_distrib_nat)
   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
     by (simp add: k_m [symmetric] k_n [symmetric])
   also have "\<dots> = k * p * q * gcd m n"
-    by (simp add: mult_ac gcd_mult_distrib_nat)
+    by (simp add: ac_simps gcd_mult_distrib_nat)
   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
     by (simp only: k_m [symmetric] k_n [symmetric])
   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
     by simp
   with prod_gcd_lcm_nat [of m n]
   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   with pos_gcd have "lcm m n * gcd q p = k" by auto
   then show ?thesis using dvd_def by auto
 qed
@@ -1353,7 +1353,7 @@
     have "gcd m n dvd n" by simp
     then obtain k where "n = gcd m n * k" using dvd_def by auto
     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
-      by (simp add: mult_ac)
+      by (simp add: ac_simps)
     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
     finally show ?thesis by (simp add: lcm_nat_def)
   qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Groups.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -169,14 +169,10 @@
 
 declare add.left_commute [algebra_simps, field_simps]
 
-theorems add_ac = add.assoc add.commute add.left_commute
-
 end
 
 hide_fact add_commute
 
-theorems add_ac = add.assoc add.commute add.left_commute
-
 class semigroup_mult = times +
   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
 begin
@@ -197,14 +193,10 @@
 
 declare mult.left_commute [algebra_simps, field_simps]
 
-theorems mult_ac = mult.assoc mult.commute mult.left_commute
-
 end
 
 hide_fact mult_commute
 
-theorems mult_ac = mult.assoc mult.commute mult.left_commute
-
 class monoid_add = zero + semigroup_add +
   assumes add_0_left: "0 + a = a"
     and add_0_right: "a + 0 = a"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Int.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -518,11 +518,11 @@
 
 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
-  unfolding Let_def ..
+  by (fact Let_numeral) -- {* FIXME drop *}
 
 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   -- {* Unfold all @{text let}s involving constants *}
-  unfolding Let_def ..
+  by (fact Let_neg_numeral) -- {* FIXME drop *}
 
 text {* Unfold @{text min} and @{text max} on numerals. *}
 
@@ -559,7 +559,7 @@
 proof -
   have "0 \<le> z" by fact
   also have "... < z + 1" by (rule less_add_one)
-  also have "... = 1 + z" by (simp add: add_ac)
+  also have "... = 1 + z" by (simp add: ac_simps)
   finally show "0 < 1 + z" .
 qed
 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/BigO.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -67,7 +67,7 @@
   apply (drule_tac x = "xa" in spec)+
   apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
   apply (erule order_trans)
-  apply (simp add: mult_ac)
+  apply (simp add: ac_simps)
   apply (rule mult_left_mono, assumption)
   apply (rule order_less_imp_le, assumption)
   done
@@ -287,7 +287,7 @@
   apply (rule mult_mono)
   apply assumption+
   apply auto
-  apply (simp add: mult_ac abs_mult)
+  apply (simp add: ac_simps abs_mult)
   done
 
 lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"
@@ -296,7 +296,7 @@
   apply auto
   apply (drule_tac x = x in spec)
   apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
-  apply (force simp add: mult_ac)
+  apply (force simp add: ac_simps)
   apply (rule mult_left_mono, assumption)
   apply (rule abs_ge_zero)
   done
@@ -328,7 +328,7 @@
   also have "(\<lambda>x. 1 / f x) * (f * g) = g"
     apply (simp add: func_times)
     apply (rule ext)
-    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
+    apply (simp add: assms nonzero_divide_eq_eq ac_simps)
     done
   finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .
   then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"
@@ -336,7 +336,7 @@
   also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"
     apply (simp add: func_times)
     apply (rule ext)
-    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
+    apply (simp add: assms nonzero_divide_eq_eq ac_simps)
     done
   finally show "h \<in> f *o O(g)" .
 qed
@@ -432,7 +432,7 @@
   apply (rule bigo_minus)
   apply (subst set_minus_plus)
   apply assumption
-  apply (simp add: add_ac)
+  apply (simp add: ac_simps)
   done
 
 lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
@@ -441,7 +441,7 @@
   done
 
 lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
-  by (auto simp add: bigo_def mult_ac)
+  by (auto simp add: bigo_def ac_simps)
 
 lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"
   apply (rule bigo_elt_subset)
@@ -536,7 +536,7 @@
   apply (rule mult_left_mono)
   apply (erule spec)
   apply simp
-  apply(simp add: mult_ac)
+  apply(simp add: ac_simps)
   done
 
 lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Discrete.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -162,7 +162,7 @@
         case True then have "mono (times q)" by (rule mono_times_nat)
         then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
           using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
-        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: mult_ac)
+        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
         then show ?thesis apply simp
           apply (subst Max_le_iff)
           apply auto
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -169,10 +169,10 @@
 lemma plus_1_eSuc:
   "1 + q = eSuc q"
   "q + 1 = eSuc q"
-  by (simp_all add: eSuc_plus_1 add_ac)
+  by (simp_all add: eSuc_plus_1 ac_simps)
 
 lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
-  by (simp_all add: eSuc_plus_1 add_ac)
+  by (simp_all add: eSuc_plus_1 ac_simps)
 
 lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
   by (simp only: add.commute[of m] iadd_Suc)
@@ -523,7 +523,7 @@
   val trans_tac = Numeral_Simprocs.trans_tac
   val norm_ss =
     simpset_of (put_simpset HOL_basic_ss @{context}
-      addsimps @{thms add_ac add_0_left add_0_right})
+      addsimps @{thms ac_simps add_0_left add_0_right})
   fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   fun simplify_meta_eq ctxt cancel_th th =
     Arith_Data.simplify_meta_eq [] ctxt
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -558,7 +558,7 @@
   then have "ln y * real k + ln x > 0"
     by simp
   then have "exp (real k * ln y + ln x) > exp 0"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   then have "y ^ k * x > 1"
     unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
     by simp
@@ -724,7 +724,7 @@
   from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp
   from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0]
   have "inverse f * f = inverse f * inverse (inverse f)"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   then show ?thesis
     using f0 unfolding mult_cancel_left by simp
 qed
@@ -736,7 +736,7 @@
 proof -
   from inverse_mult_eq_1[OF f0] fg
   have th0: "inverse f * f = g * f"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   then show ?thesis
     using f0
     unfolding mult_cancel_right
@@ -1400,7 +1400,7 @@
     using fps_divide_X_minus1_setsum_lemma[of a, symmetric] th0
     by (simp add: fps_divide_def mult.assoc)
   also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n::nat. setsum (op $ a) {0..n}) "
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   finally show ?thesis
     by (simp add: inverse_mult_eq_1[OF th0])
 qed
@@ -2074,7 +2074,7 @@
           apply (rule eq_divide_imp')
           using r00
           apply (simp del: of_nat_Suc)
-          apply (simp add: mult_ac)
+          apply (simp add: ac_simps)
           done
         then have "a$n = ?r $n"
           apply (simp del: of_nat_Suc)
@@ -2128,7 +2128,7 @@
   have "fps_deriv (?r ^ Suc k) = fps_deriv a"
     by simp
   then have "fps_deriv ?r * ?w = fps_deriv a"
-    by (simp add: fps_deriv_power mult_ac del: power_Suc)
+    by (simp add: fps_deriv_power ac_simps del: power_Suc)
   then have "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a"
     by simp
   then have "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w"
@@ -2294,7 +2294,7 @@
       setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" .
 
     have "(((fps_deriv a) oo b) * (fps_deriv b))$n = setsum (\<lambda>i. (fps_deriv b)$ (n - i) * ((fps_deriv a) oo b)$i) {0..n}"
-      unfolding fps_mult_nth by (simp add: mult_ac)
+      unfolding fps_mult_nth by (simp add: ac_simps)
     also have "\<dots> = setsum (\<lambda>i. setsum (\<lambda>j. of_nat (n - i +1) * b$(n - i + 1) * of_nat (j + 1) * a$(j+1) * (b^j)$i) {0..n}) {0..n}"
       unfolding fps_deriv_nth fps_compose_nth setsum_right_distrib mult.assoc
       apply (rule setsum.cong)
@@ -3532,7 +3532,7 @@
   apply (subst minus_divide_left)
   apply (subst eq_divide_iff)
   apply (simp del: of_nat_add of_nat_Suc)
-  apply (simp only: mult_ac)
+  apply (simp only: ac_simps)
   done
 
 lemma eq_fps_cos:
@@ -3550,7 +3550,7 @@
   apply (subst minus_divide_left)
   apply (subst eq_divide_iff)
   apply (simp del: of_nat_add of_nat_Suc)
-  apply (simp only: mult_ac)
+  apply (simp only: ac_simps)
   done
 
 lemma mult_nth_0 [simp]: "(a * b) $ 0 = a $ 0 * b $ 0"
@@ -3655,7 +3655,7 @@
 
 lemma fps_demoivre: "(fps_cos a + fps_const ii * fps_sin a)^n = fps_cos (of_nat n * a) + fps_const ii * fps_sin (of_nat n * a)"
   unfolding Eii_sin_cos[symmetric] E_power_mult
-  by (simp add: mult_ac)
+  by (simp add: ac_simps)
 
 
 subsection {* Hypergeometric series *}
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -31,11 +31,11 @@
   fix a b a' b' a'' b'' :: 'a
   assume A: "((a, b), (a', b')) \<in> fractrel"
   assume B: "((a', b'), (a'', b'')) \<in> fractrel"
-  have "b' * (a * b'') = b'' * (a * b')" by (simp add: mult_ac)
+  have "b' * (a * b'') = b'' * (a * b')" by (simp add: ac_simps)
   also from A have "a * b' = a' * b" by auto
-  also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: mult_ac)
+  also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: ac_simps)
   also from B have "a' * b'' = a'' * b'" by auto
-  also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: mult_ac)
+  also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: ac_simps)
   finally have "b' * (a * b'') = b' * (a'' * b)" .
   moreover from B have "b' \<noteq> 0" by auto
   ultimately have "a * b'' = a'' * b" by simp
@@ -288,7 +288,7 @@
           ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
         by (simp add: mult_le_cancel_right)
       also have "... = ?le (a * x) (b * x) c d"
-        by (simp add: mult_ac)
+        by (simp add: ac_simps)
       finally show ?thesis .
     qed
   } note le_factor = this
@@ -299,11 +299,11 @@
   then have "?le a b c d = ?le (a * ?D') (b * ?D') c d"
     by (rule le_factor)
   also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
     by (simp only: eq1 eq2)
   also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   also from D have "... = ?le a' b' c' d'"
     by (rule le_factor [symmetric])
   finally show "?le a b c d = ?le a' b' c' d'" .
@@ -328,7 +328,7 @@
   assumes "b \<noteq> 0"
     and "d \<noteq> 0"
   shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
-  by (simp add: less_fract_def less_le_not_le mult_ac assms)
+  by (simp add: less_fract_def less_le_not_le ac_simps assms)
 
 instance
 proof
@@ -351,7 +351,7 @@
         with ff show ?thesis by (simp add: mult_le_cancel_right)
       qed
       also have "... = (c * f) * (d * f) * (b * b)"
-        by (simp only: mult_ac)
+        by (simp only: ac_simps)
       also have "... \<le> (e * d) * (d * f) * (b * b)"
       proof -
         from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
@@ -359,7 +359,7 @@
         with bb show ?thesis by (simp add: mult_le_cancel_right)
       qed
       finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
-        by (simp only: mult_ac)
+        by (simp only: ac_simps)
       with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
         by (simp add: mult_le_cancel_right)
       with neq show ?thesis by simp
@@ -382,7 +382,7 @@
       proof -
         from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
           by simp
-        then show ?thesis by (simp only: mult_ac)
+        then show ?thesis by (simp only: ac_simps)
       qed
       finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
       moreover from neq have "b * d \<noteq> 0" by simp
@@ -469,7 +469,7 @@
       ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
         by (simp add: mult_less_cancel_right)
       with neq show ?thesis
-        by (simp add: mult_ac)
+        by (simp add: ac_simps)
     qed
   qed
 qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -732,7 +732,7 @@
     {
       fix w
       have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
-        using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
+        using qr[rule_format, of w] a00 by (simp add: divide_inverse ac_simps)
       also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
         using a00 unfolding norm_divide by (simp add: field_simps)
       finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .
@@ -980,7 +980,7 @@
                 have "p = [:- a, 1:] ^ (Suc ?op) * u"
                   apply (subst s)
                   apply (subst u)
-                  apply (simp only: power_Suc mult_ac)
+                  apply (simp only: power_Suc ac_simps)
                   done
                 with ap(2)[unfolded dvd_def] have False
                   by blast
@@ -1010,7 +1010,7 @@
               apply (subst mult.assoc [where a=u])
               apply (subst mult.assoc [where b=u, symmetric])
               apply (subst u [symmetric])
-              apply (simp add: mult_ac power_add [symmetric])
+              apply (simp add: ac_simps power_add [symmetric])
               done
             then have ?ths
               unfolding dvd_def by blast
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -280,7 +280,7 @@
      \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   unfolding gderiv_def has_field_derivative_def
   apply (drule (1) has_derivative_compose)
-  apply (simp add: mult_ac)
+  apply (simp add: ac_simps)
   done
 
 lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
@@ -313,7 +313,7 @@
   unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
   apply (rule has_derivative_subst)
   apply (erule (1) has_derivative_scaleR)
-  apply (simp add: mult_ac)
+  apply (simp add: ac_simps)
   done
 
 lemma GDERIV_mult:
@@ -322,7 +322,7 @@
   unfolding gderiv_def
   apply (rule has_derivative_subst)
   apply (erule (1) has_derivative_mult)
-  apply (simp add: inner_add mult_ac)
+  apply (simp add: inner_add ac_simps)
   done
 
 lemma GDERIV_inverse:
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -717,7 +717,7 @@
     by (blast dest: multi_member_split)
   have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
   then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" 
-    by (simp add: add_ac)
+    by (simp add: ac_simps)
   then show ?thesis using B by simp
 qed
 
@@ -817,7 +817,7 @@
 next
   case (add M x)
   have "M + {#x#} + N = (M + N) + {#x#}"
-    by (simp add: add_ac)
+    by (simp add: ac_simps)
   with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm)
 qed
 
@@ -851,7 +851,7 @@
 lemma comp_fun_commute_mset_image:
   "comp_fun_commute (plus o single o f)"
 proof
-qed (simp add: add_ac fun_eq_iff)
+qed (simp add: ac_simps fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   by (simp add: image_mset_def)
@@ -868,7 +868,7 @@
 proof -
   interpret comp_fun_commute "plus o single o f"
     by (fact comp_fun_commute_mset_image)
-  show ?thesis by (induct N) (simp_all add: image_mset_def add_ac)
+  show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
 qed
 
 corollary image_mset_insert:
@@ -956,7 +956,7 @@
 
 lemma multiset_of_append [simp]:
   "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
-  by (induct xs arbitrary: ys) (auto simp: add_ac)
+  by (induct xs arbitrary: ys) (auto simp: ac_simps)
 
 lemma multiset_of_filter:
   "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
@@ -1008,7 +1008,7 @@
 
 lemma multiset_of_compl_union [simp]:
   "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
-  by (induct xs) (auto simp: add_ac)
+  by (induct xs) (auto simp: ac_simps)
 
 lemma count_multiset_of_length_filter:
   "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
@@ -1552,7 +1552,7 @@
     next
       fix K'
       assume "M0' = K' + {#a#}"
-      with N have n: "N = K' + K + {#a#}" by (simp add: add_ac)
+      with N have n: "N = K' + K + {#a#}" by (simp add: ac_simps)
 
       assume "M0 = K' + {#a'#}"
       with r have "?R (K' + K) M0" by blast
@@ -1701,7 +1701,7 @@
 apply (simp add: mult1_def set_of_def)
 apply (rule_tac x = a in exI)
 apply (rule_tac x = "I + J'" in exI)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma one_step_implies_mult:
@@ -1840,14 +1840,14 @@
       "{#x#} + X = A + ({#y#}+Z) 
       \<and> {#y#} + Y = B + ({#y#}+Z)
       \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
-      by (auto simp: add_ac)
+      by (auto simp: ac_simps)
     thus ?case by (intro exI)
   next
     assume A: "(x, y) \<in> pair_less"
     let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
     have "{#x#} + X = ?A' + Z"
       "{#y#} + Y = ?B' + Z"
-      by (auto simp add: add_ac)
+      by (auto simp add: ac_simps)
     moreover have 
       "(set_of ?A', set_of ?B') \<in> max_strict"
       using 1 A unfolding max_strict_def 
@@ -1880,12 +1880,12 @@
       assume [simp]: "A' = {#} \<and> B' = {#}"
       show ?thesis by (rule smsI) (auto intro: max)
     qed
-    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:add_ac)
+    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:ac_simps)
     thus "(Z + A, Z' + B) \<in> ms_weak" by (simp add: ms_weak_def)
   }
   from mx_or_empty
   have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
-  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
+  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:ac_simps)
 qed
 
 lemma empty_neutral: "{#} + x = x" "x + {#} = x"
@@ -1914,7 +1914,7 @@
 
   val regroup_munion_conv =
       Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
-        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral}))
+        (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
 
   fun unfold_pwleq_tac i =
     (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -147,7 +147,7 @@
 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
 apply (induct k)
 apply (simp add: zero_def)
-apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
+apply (simp add: Rep_simps add_def one_def zmod_simps ac_simps)
 done
 
 lemma of_int_eq: "of_int z = Abs (z mod n)"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -657,7 +657,7 @@
 lemma setsum_Set [code]:
   "setsum f (Set xs) = fold_keys (plus o f) xs 0"
 proof -
-  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
+  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
   then show ?thesis 
     by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
 qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -100,11 +100,11 @@
 
 lemma set_plus_rearrange:
   "((a::'a::comm_monoid_add) +o C) + (b +o D) = (a + b) +o (C + D)"
-  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
+  apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
    apply (rule_tac x = "ba + bb" in exI)
-  apply (auto simp add: add_ac)
+  apply (auto simp add: ac_simps)
   apply (rule_tac x = "aa + a" in exI)
-  apply (auto simp add: add_ac)
+  apply (auto simp add: ac_simps)
   done
 
 lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C"
@@ -112,19 +112,19 @@
 
 lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = a +o (B + C)"
   apply (auto simp add: elt_set_plus_def set_plus_def)
-   apply (blast intro: add_ac)
+   apply (blast intro: ac_simps)
   apply (rule_tac x = "a + aa" in exI)
   apply (rule conjI)
    apply (rule_tac x = "aa" in bexI)
     apply auto
   apply (rule_tac x = "ba" in bexI)
-   apply (auto simp add: add_ac)
+   apply (auto simp add: ac_simps)
   done
 
 theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = a +o (C + D)"
-  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
+  apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
    apply (rule_tac x = "aa + ba" in exI)
-   apply (auto simp add: add_ac)
+   apply (auto simp add: ac_simps)
   done
 
 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
@@ -140,7 +140,7 @@
   by (auto simp add: elt_set_plus_def set_plus_def)
 
 lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) \<in> C \<Longrightarrow> a +o D \<subseteq> D + C"
-  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
+  by (auto simp add: elt_set_plus_def set_plus_def ac_simps)
 
 lemma set_plus_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a +o B \<subseteq> C + D"
   apply (subgoal_tac "a +o B \<subseteq> a +o D")
@@ -178,17 +178,17 @@
   apply (auto simp add: set_plus_def)
   apply (rule_tac x = 0 in bexI)
    apply (rule_tac x = x in bexI)
-    apply (auto simp add: add_ac)
+    apply (auto simp add: ac_simps)
   done
 
 lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C \<Longrightarrow> (a - b) \<in> C"
-  by (auto simp add: elt_set_plus_def add_ac)
+  by (auto simp add: elt_set_plus_def ac_simps)
 
 lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C \<Longrightarrow> a \<in> b +o C"
-  apply (auto simp add: elt_set_plus_def add_ac)
+  apply (auto simp add: elt_set_plus_def ac_simps)
   apply (subgoal_tac "a = (a + - b) + b")
    apply (rule bexI, assumption)
-  apply (auto simp add: add_ac)
+  apply (auto simp add: ac_simps)
   done
 
 lemma set_minus_plus: "(a::'a::ab_group_add) - b \<in> C \<longleftrightarrow> a \<in> b +o C"
@@ -209,9 +209,9 @@
   "((a::'a::comm_monoid_mult) *o C) * (b *o D) = (a * b) *o (C * D)"
   apply (auto simp add: elt_set_times_def set_times_def)
    apply (rule_tac x = "ba * bb" in exI)
-   apply (auto simp add: mult_ac)
+   apply (auto simp add: ac_simps)
   apply (rule_tac x = "aa * a" in exI)
-  apply (auto simp add: mult_ac)
+  apply (auto simp add: ac_simps)
   done
 
 lemma set_times_rearrange2:
@@ -221,20 +221,20 @@
 lemma set_times_rearrange3:
   "((a::'a::semigroup_mult) *o B) * C = a *o (B * C)"
   apply (auto simp add: elt_set_times_def set_times_def)
-   apply (blast intro: mult_ac)
+   apply (blast intro: ac_simps)
   apply (rule_tac x = "a * aa" in exI)
   apply (rule conjI)
    apply (rule_tac x = "aa" in bexI)
     apply auto
   apply (rule_tac x = "ba" in bexI)
-   apply (auto simp add: mult_ac)
+   apply (auto simp add: ac_simps)
   done
 
 theorem set_times_rearrange4:
   "C * ((a::'a::comm_monoid_mult) *o D) = a *o (C * D)"
-  apply (auto simp add: elt_set_times_def set_times_def mult_ac)
+  apply (auto simp add: elt_set_times_def set_times_def ac_simps)
    apply (rule_tac x = "aa * ba" in exI)
-   apply (auto simp add: mult_ac)
+   apply (auto simp add: ac_simps)
   done
 
 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
@@ -250,7 +250,7 @@
   by (auto simp add: elt_set_times_def set_times_def)
 
 lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C \<Longrightarrow> a *o D \<subseteq> D * C"
-  by (auto simp add: elt_set_times_def set_times_def mult_ac)
+  by (auto simp add: elt_set_times_def set_times_def ac_simps)
 
 lemma set_times_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a *o B \<subseteq> C * D"
   apply (subgoal_tac "a *o B \<subseteq> a *o D")
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/List.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -2104,13 +2104,13 @@
 by (simp add: butlast_conv_take min.absorb1 min.absorb2)
 
 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
-by (simp add: butlast_conv_take drop_take add_ac)
+by (simp add: butlast_conv_take drop_take ac_simps)
 
 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
 by (simp add: butlast_conv_take min.absorb1)
 
 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
-by (simp add: butlast_conv_take drop_take add_ac)
+by (simp add: butlast_conv_take drop_take ac_simps)
 
 lemma hd_drop_conv_nth: "n < length xs \<Longrightarrow> hd(drop n xs) = xs!n"
 by(simp add: hd_conv_nth)
@@ -3471,7 +3471,7 @@
 
 lemma (in comm_monoid_add) listsum_rev [simp]:
   "listsum (rev xs) = listsum xs"
-  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
+  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff ac_simps)
 
 lemma (in monoid_add) fold_plus_listsum_rev:
   "fold plus xs = plus (listsum (rev xs))"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/MacLaurin.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -574,7 +574,7 @@
     apply (rule setsum.cong[OF refl])
     apply (subst diff_m_0, simp)
     apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
-                simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult)
+                simp add: est ac_simps divide_inverse power_abs [symmetric] abs_mult)
     done
 qed
 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -301,7 +301,7 @@
 lemma bigo_mult [intro]: "O(f) * O(g) <= O(f * g)"
 apply (rule subsetI)
 apply (subst bigo_def)
-apply (auto simp del: abs_mult mult_ac
+apply (auto simp del: abs_mult ac_simps
             simp add: bigo_alt_def set_times_def func_times)
 (* sledgehammer *)
 apply (rule_tac x = "c * ca" in exI)
@@ -334,7 +334,7 @@
       by (rule bigo_mult2)
     also have "(\<lambda>x. 1 / f x) * (f * g) = g"
       apply (simp add: func_times)
-      by (metis (lifting, no_types) a ext mult_ac(2) nonzero_divide_eq_eq)
+      by (metis (lifting, no_types) a ext mult.commute nonzero_divide_eq_eq)
     finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
     then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
       by auto
@@ -396,7 +396,7 @@
 by (metis bigo_add_commute_imp)
 
 lemma bigo_const1: "(\<lambda>x. c) : O(\<lambda>x. 1)"
-by (auto simp add: bigo_def mult_ac)
+by (auto simp add: bigo_def ac_simps)
 
 lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<le> O(\<lambda>x. 1)"
 by (metis bigo_const1 bigo_elt_subset)
@@ -462,13 +462,13 @@
   hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
     by (metis comm_mult_left_mono)
   thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
-    using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
+    using A2 F4 by (metis mult.assoc comm_mult_left_mono)
 qed
 
 lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
   apply (auto intro!: subsetI
     simp add: bigo_def elt_set_times_def func_times
-    simp del: abs_mult mult_ac)
+    simp del: abs_mult ac_simps)
 (* sledgehammer *)
   apply (rule_tac x = "ca * (abs c)" in exI)
   apply (rule allI)
@@ -478,7 +478,7 @@
   apply (rule mult_left_mono)
   apply (erule spec)
   apply simp
-  apply (simp add: mult_ac)
+  apply (simp add: ac_simps)
 done
 
 lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -418,7 +418,7 @@
   by (simp add: matrix_vector_mult_def inner_vec_def)
 
 lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
-  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
+  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib ac_simps)
   apply (subst setsum.commute)
   apply simp
   done
@@ -525,7 +525,7 @@
   apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
     setsum_left_distrib setsum_right_distrib)
   apply (subst setsum.commute)
-  apply (auto simp add: mult_ac)
+  apply (auto simp add: ac_simps)
   done
 
 lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
@@ -1221,7 +1221,7 @@
   unfolding UNIV_2 by simp
 
 lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
-  unfolding UNIV_3 by (simp add: add_ac)
+  unfolding UNIV_3 by (simp add: ac_simps)
 
 instantiation num1 :: cart_one
 begin
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1019,7 +1019,7 @@
                    (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
                    (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
                    (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
-          by (simp only: fact_Suc of_nat_mult mult_ac) simp
+          by (simp only: fact_Suc of_nat_mult ac_simps) simp
         also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
           by (simp add: algebra_simps)
         finally show ?thesis
@@ -1116,7 +1116,7 @@
              (\<Sum>i = 0..n.
                  f (Suc (Suc i)) u * ((z-u) ^ Suc i) / of_nat (fact (Suc i))  - 
                  f (Suc i) u * (z-u) ^ i / of_nat (fact i))"
-      by (simp only: diff_divide_distrib fact_cancel mult_ac)
+      by (simp only: diff_divide_distrib fact_cancel ac_simps)
     also have "... = f (Suc 0) u -
              (f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
              of_nat (fact (Suc n)) +
@@ -1132,7 +1132,7 @@
       apply (intro derivative_eq_intros)+
       apply (force intro: u assms)
       apply (rule refl)+
-      apply (auto simp: mult_ac)
+      apply (auto simp: ac_simps)
       done
   }
   then show ?thesis
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -476,7 +476,7 @@
   also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
     by (simp add: field_simps)
   also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"
-    unfolding th1 by (simp add: mult_ac)
+    unfolding th1 by (simp add: ac_simps)
   also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
     unfolding setprod.insert[OF th3] by simp
   finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)"
@@ -824,7 +824,7 @@
         by (simp_all add: sign_idempotent)
       have ths: "?s q = ?s p * ?s (q \<circ> inv p)"
         using pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
-        by (simp add:  th00 mult_ac sign_idempotent sign_compose)
+        by (simp add:  th00 ac_simps sign_idempotent sign_compose)
       have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U"
         by (rule setprod_permute[OF p])
       have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1578,7 +1578,7 @@
     have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
       using `bilinear h` by (rule bilinear_bounded)
     then show "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
-      by (simp add: mult_ac)
+      by (simp add: ac_simps)
   qed
 next
   assume "bounded_bilinear h"
@@ -1597,7 +1597,7 @@
     using bh [unfolded bilinear_conv_bounded_bilinear]
     by (rule bounded_bilinear.pos_bounded)
   then show ?thesis
-    by (simp only: mult_ac)
+    by (simp only: ac_simps)
 qed
 
 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Multivariate_Analysis/PolyRoots.thy
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -41,9 +41,9 @@
   shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
 proof -
   have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
-    by (metis ab_semigroup_mult_class.mult_ac(1) assms mult.commute setsum_power_shift)
+    by (metis mult.assoc mult.commute assms setsum_power_shift)
   also have "... =x^m * (1 - x^Suc(n-m))"
-    by (metis ab_semigroup_mult_class.mult_ac(1) setsum_gp_basic)
+    by (metis mult.assoc setsum_gp_basic)
   also have "... = x^m - x^Suc n"
     using assms
     by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
@@ -78,9 +78,9 @@
         (\<Sum>i\<le>n. a i * (x^i - y^i))"
     by (simp add: algebra_simps setsum_subtractf [symmetric])
   also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
-    by (simp add: power_diff_sumr2 mult_ac)
+    by (simp add: power_diff_sumr2 ac_simps)
   also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
-    by (simp add: setsum_right_distrib mult_ac)
+    by (simp add: setsum_right_distrib ac_simps)
   also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
     by (simp add: nested_setsum_swap')
   finally show ?thesis .
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -2844,7 +2844,7 @@
   from assms(1) obtain b where b: "b > 0" "\<forall>x\<in>S. norm x \<le> b"
     unfolding bounded_pos by auto
   from assms(2) obtain B where B: "B > 0" "\<forall>x. norm (f x) \<le> B * norm x"
-    using bounded_linear.pos_bounded by (auto simp add: mult_ac)
+    using bounded_linear.pos_bounded by (auto simp add: ac_simps)
   {
     fix x
     assume "x \<in> S"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/NSA/CLim.thy
--- a/src/HOL/NSA/CLim.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NSA/CLim.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -142,7 +142,7 @@
 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
 apply (auto simp add: distrib_right real_of_nat_Suc)
 apply (case_tac "n")
-apply (auto simp add: mult_ac add.commute)
+apply (auto simp add: ac_simps add.commute)
 done
 
 text{*Nonstandard version*}
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NSA/HDeriv.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -171,7 +171,7 @@
 apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
 apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
 apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
-apply (auto simp add: add_ac algebra_simps)
+apply (auto simp add: ac_simps algebra_simps)
 done
 
 text{*Product of functions - Proof is trivial but tedious
@@ -180,7 +180,7 @@
 lemma lemma_nsderiv1:
   fixes a b c d :: "'a::comm_ring star"
   shows "(a*b) - (c*d) = (b*(a - c)) + (c*(b - d))"
-by (simp add: right_diff_distrib mult_ac)
+by (simp add: right_diff_distrib ac_simps)
 
 lemma lemma_nsderiv2:
   fixes x y z :: "'a::real_normed_field star"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NSA/HTranscendental.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -527,7 +527,7 @@
                    pi_divide_HNatInfinite_not_zero])
 apply (auto)
 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
-apply (auto intro: Reals_inverse simp add: divide_inverse mult_ac)
+apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps)
 done
 
 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NSA/NSA.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -776,7 +776,7 @@
 
 lemma approx_add_left_cancel: "d + b  @= d + c ==> b @= c"
 apply (drule approx_minus_iff [THEN iffD1])
-apply (simp add: approx_minus_iff [symmetric] add_ac)
+apply (simp add: approx_minus_iff [symmetric] ac_simps)
 done
 
 lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
@@ -786,7 +786,7 @@
 
 lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
 apply (rule approx_minus_iff [THEN iffD2])
-apply (simp add: approx_minus_iff [symmetric] add_ac)
+apply (simp add: approx_minus_iff [symmetric] ac_simps)
 done
 
 lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
@@ -1714,25 +1714,25 @@
 lemma Infinitesimal_sum_square_cancel2 [simp]:
      "(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
 apply (rule Infinitesimal_sum_square_cancel)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma HFinite_sum_square_cancel2 [simp]:
      "(y::hypreal)*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
 apply (rule HFinite_sum_square_cancel)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma Infinitesimal_sum_square_cancel3 [simp]:
      "(z::hypreal)*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
 apply (rule Infinitesimal_sum_square_cancel)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma HFinite_sum_square_cancel3 [simp]:
      "(z::hypreal)*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
 apply (rule HFinite_sum_square_cancel)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma monad_hrabs_less:
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Nat.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1075,10 +1075,10 @@
 lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
 by (blast dest: add_leD1 add_leD2)
 
-text {* needs @{text "!!k"} for @{text add_ac} to work *}
+text {* needs @{text "!!k"} for @{text ac_simps} to work *}
 lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
 by (force simp del: add_Suc_right
-    simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
+    simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
 
 
 subsubsection {* More results about difference *}
@@ -1405,10 +1405,10 @@
   by (simp add: of_nat_def)
 
 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
-  by (induct m) (simp_all add: add_ac)
+  by (induct m) (simp_all add: ac_simps)
 
 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
-  by (induct m) (simp_all add: add_ac distrib_right)
+  by (induct m) (simp_all add: ac_simps distrib_right)
 
 primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   "of_nat_aux inc 0 i = i"
@@ -1869,7 +1869,7 @@
 lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
   unfolding dvd_def
   apply (erule exE)
-  apply (simp add: mult_ac)
+  apply (simp add: ac_simps)
   done
 
 lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NthRoot.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -527,7 +527,7 @@
 lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
 apply (simp add: divide_inverse)
 apply (case_tac "r=0")
-apply (auto simp add: mult_ac)
+apply (auto simp add: ac_simps)
 done
 
 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -161,7 +161,7 @@
     by (rule distrib)
   also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
                   (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
-    by (auto simp add: setsum_right_distrib mult_ac)
+    by (auto simp add: setsum_right_distrib ac_simps)
   also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
                   (\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
     by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps  
@@ -634,7 +634,7 @@
   also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
     apply (subst div_mult_div_if_dvd)
     apply (auto simp: fact_fact_dvd_fact)
-    apply (metis ab_semigroup_add_class.add_ac(1) add.commute fact_fact_dvd_fact)
+    apply (metis ac_simps add.commute fact_fact_dvd_fact)
     done
   also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
     apply (subst div_mult_div_if_dvd [symmetric])
@@ -758,7 +758,7 @@
     also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
       by(subst setsum_right_distrib[symmetric]) simp
     also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
-      by(subst binomial_ring)(simp add: mult_ac)
+      by(subst binomial_ring)(simp add: ac_simps)
     also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
     finally show "?lhs x = 1" .
   qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -115,7 +115,7 @@
   apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   apply auto
 (* auto should get this. I suppose we need "comm_monoid_simprules"
-   for mult_ac rewriting. *)
+   for ac_simps rewriting. *)
   apply (subst m_assoc [symmetric])
   apply auto
   done
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -549,7 +549,7 @@
   from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
   hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
   with k l have "a ^ (q * r) = p*l*k + 1" by simp
-  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
+  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
   hence odq: "ord p (a^r) dvd q"
     unfolding ord_divides[symmetric] power_mult[symmetric]
     by (metis an cong_dvd_modulus_nat mult.commute nqr pn) 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -40,7 +40,7 @@
   apply (insert m_gt_one)
   apply (rule abelian_groupI)
   apply (unfold R_def residue_ring_def)
-  apply (auto simp add: mod_add_right_eq [symmetric] add_ac)
+  apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
   apply (case_tac "x = 0")
   apply force
   apply (subgoal_tac "(x + (m - x)) mod m = 0")
@@ -56,7 +56,7 @@
   apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
   apply (erule ssubst)
   apply (subst mod_mult_right_eq [symmetric])+
-  apply (simp_all only: mult_ac)
+  apply (simp_all only: ac_simps)
   done
 
 lemma cring: "cring R"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/Chinese.thy
--- a/src/HOL/Old_Number_Theory/Chinese.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -238,7 +238,7 @@
           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
          prefer 6
-         apply (simp add: mult_ac)
+         apply (simp add: ac_simps)
         apply (unfold xilin_sol_def)
         apply (tactic {* asm_simp_tac @{context} 6 *})
         apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -67,7 +67,7 @@
   then have "[j * j = (a * MultInv p j) * j] (mod p)"
     by (auto simp add: zcong_scalar)
   then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
-    by (auto simp add: mult_ac)
+    by (auto simp add: ac_simps)
   have "[j * j = a] (mod p)"
   proof -
     from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
@@ -149,7 +149,7 @@
                    c = "a * (x * MultInv p x)" in  zcong_trans, force)
   apply (frule_tac p = p and x = x in MultInv_prop2, auto)
 apply (metis StandardRes_SRStar_prop3 mult_1_right mult.commute zcong_sym zcong_zmult_prop1)
-  apply (auto simp add: mult_ac)
+  apply (auto simp add: ac_simps)
   done
 
 lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -255,7 +255,7 @@
   apply (subst setprod.insert)
     apply (rule_tac [2] Bnor_prod_power_aux)
      apply (unfold inj_on_def)
-     apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)
+     apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap)
   done
 
 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/Factorization.thy
--- a/src/HOL/Old_Number_Theory/Factorization.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -188,7 +188,7 @@
 
 lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
   apply (induct set: perm)
-     apply (simp_all add: mult_ac)
+     apply (simp_all add: ac_simps)
   done
 
 lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/Int2.thy
--- a/src/HOL/Old_Number_Theory/Int2.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -51,7 +51,7 @@
   have "(x div z) * z \<le> (x div z) * z" by simp
   then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
   also have "\<dots> = x"
-    by (auto simp add: zmod_zdiv_equality [symmetric] mult_ac)
+    by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps)
   also note `x < y * z`
   finally show ?thesis
     apply (auto simp add: mult_less_cancel_right)
@@ -115,7 +115,7 @@
 
 lemma zcong_zmult_prop2: "[a = b](mod m) ==>
     ([c = d * a](mod m) = [c = d * b] (mod m))"
-  by (auto simp add: mult_ac zcong_zmult_prop1)
+  by (auto simp add: ac_simps zcong_zmult_prop1)
 
 lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
     ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
@@ -198,7 +198,7 @@
 
 lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
     [(MultInv p x) * x = 1] (mod p)"
-  by (auto simp add: MultInv_prop2 mult_ac)
+  by (auto simp add: MultInv_prop2 ac_simps)
 
 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
   by (simp add: nat_diff_distrib)
@@ -227,7 +227,7 @@
   apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
   apply (drule MultInv_prop2, auto)
   apply (drule_tac k = x in zcong_scalar2, auto)
-  apply (auto simp add: mult_ac)
+  apply (auto simp add: ac_simps)
   done
 
 lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
@@ -244,10 +244,10 @@
     m = p and k = x in zcong_scalar)
   apply (insert MultInv_prop2 [of p x], simp)
   apply (auto simp only: zcong_sym [of "MultInv p x * x"])
-  apply (auto simp add: mult_ac)
+  apply (auto simp add: ac_simps)
   apply (drule zcong_trans, auto)
   apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
-  apply (insert MultInv_prop2a [of p y], auto simp add: mult_ac)
+  apply (insert MultInv_prop2a [of p y], auto simp add: ac_simps)
   apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
   apply (auto simp add: zcong_sym)
   done
@@ -264,7 +264,7 @@
     [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
   apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
     [of "MultInv p k * k" 1 p "j * k" a])
-  apply (auto simp add: mult_ac)
+  apply (auto simp add: ac_simps)
   done
 
 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
@@ -276,7 +276,7 @@
        ==> [k = a * (MultInv p j)] (mod p)"
   apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
     [of "MultInv p j * j" 1 p "MultInv p j * a" k])
-  apply (auto simp add: mult_ac zcong_sym)
+  apply (auto simp add: ac_simps zcong_sym)
   done
 
 lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -253,7 +253,7 @@
 
 lemma zcong_zmod_aux:
      "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
-  by(simp add: right_diff_distrib add_diff_eq eq_diff_eq add_ac)
+  by(simp add: right_diff_distrib add_diff_eq eq_diff_eq ac_simps)
 
 lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
   apply (unfold zcong_def)
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -351,7 +351,7 @@
           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
-            by (simp only: diff_mult_distrib2 add.commute mult_ac)
+            by (simp only: diff_mult_distrib2 add.commute ac_simps)
           hence ?thesis using H(1,2)
             apply -
             apply (rule exI[where x=d], simp)
@@ -492,20 +492,20 @@
   from pos_k k_m have pos_p: "p > 0" by auto
   from pos_k k_n have pos_q: "q > 0" by auto
   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
-    by (simp add: mult_ac gcd_mult_distrib2)
+    by (simp add: ac_simps gcd_mult_distrib2)
   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
     by (simp add: k_m [symmetric] k_n [symmetric])
   also have "\<dots> = k * p * q * gcd m n"
-    by (simp add: mult_ac gcd_mult_distrib2)
+    by (simp add: ac_simps gcd_mult_distrib2)
   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
     by (simp only: k_m [symmetric] k_n [symmetric])
   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
     by simp
   with prod_gcd_lcm [of m n]
   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
-    by (simp add: mult_ac)
+    by (simp add: ac_simps)
   with pos_gcd have "lcm m n * gcd q p = k" by simp
   then show ?thesis using dvd_def by auto
 qed
@@ -525,7 +525,7 @@
     then have npos: "n > 0" by simp
     have "gcd m n dvd n" by simp
     then obtain k where "n = gcd m n * k" using dvd_def by auto
-    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
+    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: ac_simps)
     also have "\<dots> = m * k" using mpos npos gcd_zero by simp
     finally show ?thesis by (simp add: lcm_def)
   qed
@@ -546,7 +546,7 @@
     then have mpos: "m > 0" by simp
     have "gcd m n dvd m" by simp
     then obtain k where "m = gcd m n * k" using dvd_def by auto
-    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
+    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: ac_simps)
     also have "\<dots> = n * k" using mpos npos gcd_zero by simp
     finally show ?thesis by (simp add: lcm_def)
   qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1020,7 +1020,7 @@
   from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
   hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
   with k l have "a ^ (q * r) = p*l*k + 1" by simp
-  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
+  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
   hence odq: "ord p (a^r) dvd q"
     unfolding ord_divides[symmetric] power_mult[symmetric] nat_mod  by blast
   from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -227,10 +227,10 @@
 apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all)
 apply (rule_tac x="x" in exI)
 apply (rule_tac x="a*y" in exI)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
 apply (rule_tac x="a*x" in exI)
 apply (rule_tac x="y" in exI)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
 done
 
 lemma coprime_rmul2: "coprime d (a * b) \<Longrightarrow> coprime d a"
@@ -239,10 +239,10 @@
 apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all)
 apply (rule_tac x="x" in exI)
 apply (rule_tac x="b*y" in exI)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
 apply (rule_tac x="b*x" in exI)
 apply (rule_tac x="y" in exI)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
 done
 lemma coprime_mul_eq: "coprime d (a * b) \<longleftrightarrow> coprime d a \<and>  coprime d b"
   using coprime_rmul2[of d a b] coprime_lmul2[of d a b] coprime_mul[of d a b] 
@@ -288,7 +288,7 @@
   moreover
   {assume z: "?g \<noteq> 0"
     from gcd_dvd1[of a b] gcd_dvd2[of a b] obtain a' b' where
-      ab': "a = a'*?g" "b = b'*?g" unfolding dvd_def by (auto simp add: mult_ac)
+      ab': "a = a'*?g" "b = b'*?g" unfolding dvd_def by (auto simp add: ac_simps)
     hence ab'': "?g*a' = a" "?g * b' = b" by algebra+
     from coprime_exp_imp[OF gcd_coprime[OF z ab'], unfolded coprime_bezout, of n]
     obtain x y where "a'^n * x - b'^n * y = 1 \<or> b'^n * x - a'^n * y = 1"  by blast
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -388,7 +388,7 @@
     by (auto simp add: int_distrib)
   then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
     apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
-    by (auto simp add: even3, auto simp add: mult_ac)
+    by (auto simp add: even3, auto simp add: ac_simps)
   also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
     by (auto simp add: even1 even_prod_div_2)
   also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
@@ -557,11 +557,11 @@
 
 lemma S1_carda: "int (card(S1)) =
     setsum (%j. (j * q) div p) P_set"
-  by (auto simp add: S1_card mult_ac)
+  by (auto simp add: S1_card ac_simps)
 
 lemma S2_carda: "int (card(S2)) =
     setsum (%j. (j * p) div q) Q_set"
-  by (auto simp add: S2_card mult_ac)
+  by (auto simp add: S2_card ac_simps)
 
 lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
     (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Power.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -110,7 +110,7 @@
 
 lemma power_mult_distrib [field_simps]:
   "(a * b) ^ n = (a ^ n) * (b ^ n)"
-  by (induct n) (simp_all add: mult_ac)
+  by (induct n) (simp_all add: ac_simps)
 
 end
 
@@ -562,7 +562,7 @@
 next
   case (Suc n)
   have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
-    by (simp add: mult_ac power_add power2_eq_square)
+    by (simp add: ac_simps power_add power2_eq_square)
   thus ?case
     by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
 qed
@@ -580,7 +580,7 @@
 next
   case (Suc n)
     have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
-      by (simp add: mult_ac power_add power2_eq_square)
+      by (simp add: ac_simps power_add power2_eq_square)
     thus ?case
       by (simp add: Suc zero_le_mult_iff)
 qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Presburger.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -185,7 +185,7 @@
 proof
   assume ?LHS
   then obtain x where P: "P x" ..
-  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
+  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality ac_simps eq_diff_eq)
   hence Pmod: "P x = P(x mod d)" using modd by simp
   show ?RHS
   proof (cases)
@@ -307,7 +307,7 @@
   {fix x
     have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
     also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
-      by (simp add:int_distrib add_ac)
+      by (simp add:int_distrib ac_simps)
     ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
   thus ?case ..
 qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -475,7 +475,7 @@
     by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ereal (f x)" and v=real])
        (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
              intro!: setsum.cong ereal_cong_mult
-             simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] mult_ac
+             simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] ac_simps
              simp del: setsum_ereal times_ereal.simps(1))
   also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
     using f
@@ -631,7 +631,7 @@
       (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
     proof (intro always_eventually allI)
       fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x - s i x) \<partial>M)"
-        using K by (intro nn_integral_mono) (auto simp: mult_ac)
+        using K by (intro nn_integral_mono) (auto simp: ac_simps)
       also have "\<dots> = ?g i"
         using K by (intro nn_integral_cmult) auto
       finally show "?f i \<le> ?g i" .
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -136,7 +136,7 @@
   shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
     (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
   by (subst measurable_restrict_space_iff)
-     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] mult_ac cong del: if_cong)
+     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps cong del: if_cong)
 
 lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
   by (auto intro: borel_closed)
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Probability/Convolution.thy
--- a/src/HOL/Probability/Convolution.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Convolution.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -41,7 +41,7 @@
   assumes [simp]: "space M = space N" "space N = space borel"
   shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. (emeasure N {a. a + x \<in> A}) \<partial>M "
   using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution 
-    nn_integral_indicator[symmetric] ab_semigroup_add_class.add_ac split:split_indicator)
+    nn_integral_indicator [symmetric] ac_simps split:split_indicator)
 
 lemma convolution_emeasure':
   assumes [simp]:"A \<in> sets borel"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -33,7 +33,7 @@
     by (auto simp add: field_simps)
 
   have eq: "\<And>x. ereal \<bar>c\<bar> * (f x / ereal \<bar>c\<bar>) = f x"
-    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
+    using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
     
   have "density lborel f = distr M lborel X"
     using f by (simp add: distributed_def)
@@ -49,7 +49,7 @@
   shows "distributed M lborel X f"
 proof -
   have eq: "\<And>x. f x * ereal \<bar>c\<bar> / ereal \<bar>c\<bar> = f x"
-    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
+    using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
 
   show ?thesis
     using distributed_affine[OF f c, where t=t] c
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1270,7 +1270,7 @@
   assumes "!!x. DERIV G x :> g x"
   shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
             =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" 
-  using integral_by_parts[OF assms] by (simp add: mult_ac)
+  using integral_by_parts[OF assms] by (simp add: ac_simps)
 
 lemma has_bochner_integral_even_function:
   fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -92,7 +92,7 @@
         from m have "0 < m" by simp
         moreover note n
         moreover from False n nmk k have "Suc 0 < k" by auto
-        moreover from nmk have "k * m = n" by (simp only: mult_ac)
+        moreover from nmk have "k * m = n" by (simp only: ac_simps)
         ultimately have mn: "m < n" by (rule prod_mn_less_k)
         with kn A nmk show ?thesis by iprover
       qed
@@ -118,7 +118,7 @@
   next
     assume "m = Suc n"
     then have "m dvd (fact n * Suc n)"
-      by (auto intro: dvdI simp: mult_ac)
+      by (auto intro: dvdI simp: ac_simps)
     then show ?thesis by (simp add: mult.commute)
   qed
 qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -60,7 +60,7 @@
   apply(hypsubst_thin)
   apply(rename_tac u v w x y z)
   apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-  apply(simp add: mult_ac)
+  apply(simp add: ac_simps)
   apply(simp add: add_mult_distrib [symmetric])
 done
 
@@ -73,7 +73,7 @@
   apply(hypsubst_thin)
   apply(rename_tac u v w x y z)
   apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-  apply(simp add: mult_ac)
+  apply(simp add: ac_simps)
   apply(simp add: add_mult_distrib [symmetric])
 done
 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Rat.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -118,7 +118,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: distrib_right, simp add: mult_ac)
+  by (clarsimp, simp add: distrib_right, simp add: ac_simps)
 
 lemma add_rat [simp]:
   assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -144,7 +144,7 @@
 
 lift_definition times_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
   is "\<lambda>x y. (fst x * fst y, snd x * snd y)"
-  by (simp add: mult_ac)
+  by (simp add: ac_simps)
 
 lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)"
   by transfer simp
@@ -271,7 +271,7 @@
   proof -
     assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q"
     then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp
-    with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0)
+    with assms show "p * s = q * r" by (auto simp add: ac_simps sgn_times sgn_0_0)
   qed
   from assms show ?thesis
     by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times split: if_splits intro: aux)
@@ -413,7 +413,7 @@
   hence "a * d * b * d = c * b * b * d"
     by simp
   hence "a * b * d\<^sup>2 = c * d * b\<^sup>2"
-    unfolding power2_eq_square by (simp add: mult_ac)
+    unfolding power2_eq_square by (simp add: ac_simps)
   hence "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2"
     by simp
   thus "0 < a * b \<longleftrightarrow> 0 < c * d"
@@ -434,7 +434,7 @@
 
 lemma positive_mult:
   "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
-by transfer (drule (1) mult_pos_pos, simp add: mult_ac)
+by transfer (drule (1) mult_pos_pos, simp add: ac_simps)
 
 lemma positive_minus:
   "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
@@ -676,7 +676,7 @@
 
 lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
 apply transfer
-apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac)
+apply (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps)
 done
 
 lemma nonzero_of_rat_inverse:
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Real.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -474,9 +474,9 @@
 instance proof
   fix a b c :: real
   show "a + b = b + a"
-    by transfer (simp add: add_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "(a + b) + c = a + (b + c)"
-    by transfer (simp add: add_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "0 + a = a"
     by transfer (simp add: realrel_def)
   show "- a + a = 0"
@@ -484,11 +484,11 @@
   show "a - b = a + - b"
     by (rule minus_real_def)
   show "(a * b) * c = a * (b * c)"
-    by transfer (simp add: mult_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "a * b = b * a"
-    by transfer (simp add: mult_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "1 * a = a"
-    by transfer (simp add: mult_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "(a + b) * c = a * c + b * c"
     by transfer (simp add: distrib_right realrel_def)
   show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
@@ -707,7 +707,7 @@
   shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
 unfolding not_less [symmetric, where 'a=real] less_real_def
 apply (simp add: diff_Real not_positive_Real X Y)
-apply (simp add: diff_le_eq add_ac)
+apply (simp add: diff_le_eq ac_simps)
 done
 
 lemma le_RealI:
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -897,7 +897,7 @@
   also have "norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
     using insert by auto
   finally show ?case
-    by (auto simp add: add_ac mult_right_mono mult_left_mono)
+    by (auto simp add: ac_simps mult_right_mono mult_left_mono)
 qed simp_all
 
 lemma norm_power_diff: 
@@ -1159,7 +1159,7 @@
 
 lemma sgn_scaleR:
   "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
-by (simp add: sgn_div_norm mult_ac)
+by (simp add: sgn_div_norm ac_simps)
 
 lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
 by (simp add: sgn_div_norm)
@@ -1308,7 +1308,7 @@
 apply (rule_tac K="norm b * K" in bounded_linear_intro)
 apply (rule add_left)
 apply (rule scaleR_left)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
 done
 
 lemma bounded_linear_right:
@@ -1317,7 +1317,7 @@
 apply (rule_tac K="norm a * K" in bounded_linear_intro)
 apply (rule add_right)
 apply (rule scaleR_right)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
 done
 
 lemma prod_diff_prod:
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Rings.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -21,7 +21,7 @@
 text{*For the @{text combine_numerals} simproc*}
 lemma combine_common_factor:
   "a * e + (b * e + c) = (a + b) * e + c"
-by (simp add: distrib_right add_ac)
+by (simp add: distrib_right ac_simps)
 
 end
 
@@ -55,9 +55,9 @@
 proof
   fix a b c :: 'a
   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
-  have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
+  have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)
   also have "... = b * a + c * a" by (simp only: distrib)
-  also have "... = a * b + a * c" by (simp add: mult_ac)
+  also have "... = a * b + a * c" by (simp add: ac_simps)
   finally show "a * (b + c) = a * b + a * c" by blast
 qed
 
@@ -180,7 +180,7 @@
 proof -
   from `a dvd b` obtain b' where "b = a * b'" ..
   moreover from `c dvd d` obtain d' where "d = c * d'" ..
-  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
+  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps)
   then show ?thesis ..
 qed
 
@@ -188,7 +188,7 @@
 by (simp add: dvd_def mult.assoc, blast)
 
 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
-  unfolding mult_ac [of a] by (rule dvd_mult_left)
+  unfolding mult.commute [of a] by (rule dvd_mult_left)
 
 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
 by simp
@@ -437,7 +437,7 @@
   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
 proof -
   have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
-    unfolding dvd_def by (simp add: mult_ac)
+    unfolding dvd_def by (simp add: ac_simps)
   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
     unfolding dvd_def by simp
   finally show ?thesis .
@@ -447,7 +447,7 @@
   "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
 proof -
   have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
-    unfolding dvd_def by (simp add: mult_ac)
+    unfolding dvd_def by (simp add: ac_simps)
   also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
     unfolding dvd_def by simp
   finally show ?thesis .
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -26,7 +26,7 @@
 proof -
   from `0 \<le> c` `0 < d` `c - c sdiv d * d = 0`
   have "d dvd c"
-    by (auto simp add: sdiv_pos_pos dvd_def mult_ac)
+    by (auto simp add: sdiv_pos_pos dvd_def ac_simps)
   with `0 < d` `gcd c d = gcd m n` show ?C1
     by simp
 qed
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Semiring_Normalization.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -47,7 +47,7 @@
     then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
     then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero)
     then show "w = x \<or> y = z" by auto
-  qed (auto simp add: add_ac)
+  qed (auto simp add: ac_simps)
 qed
 
 instance nat :: comm_semiring_1_cancel_crossproduct
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Set_Interval.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1409,22 +1409,22 @@
 on intervals are not? *)
 
 lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)"
-by (simp add:atMost_Suc add_ac)
+by (simp add:atMost_Suc ac_simps)
 
 lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
-by (simp add:lessThan_Suc add_ac)
+by (simp add:lessThan_Suc ac_simps)
 
 lemma setsum_cl_ivl_Suc[simp]:
   "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
-by (auto simp:add_ac atLeastAtMostSuc_conv)
+by (auto simp:ac_simps atLeastAtMostSuc_conv)
 
 lemma setsum_op_ivl_Suc[simp]:
   "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
-by (auto simp:add_ac atLeastLessThanSuc)
+by (auto simp:ac_simps atLeastLessThanSuc)
 (*
 lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
     (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
-by (auto simp:add_ac atLeastAtMostSuc_conv)
+by (auto simp:ac_simps atLeastAtMostSuc_conv)
 *)
 
 lemma setsum_head:
@@ -1468,7 +1468,7 @@
 shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
 using setsum_add_nat_ivl [of m n p f,symmetric]
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma setsum_natinterval_difff:
@@ -1600,15 +1600,15 @@
   also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
   also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
     unfolding One_nat_def
-    by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
+    by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt ac_simps)
   also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
     by (simp add: algebra_simps)
   also from ngt1 have "{1..<n} = {1..n - 1}"
     by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
   also from ngt1
   have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
-    by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
-       (simp add:  mult_ac trans [OF add.commute of_nat_Suc [symmetric]])
+    by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)
+      (simp add:  mult.commute trans [OF add.commute of_nat_Suc [symmetric]])
   finally show ?thesis
     unfolding mult_2 by (simp add: algebra_simps)
 next
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Jul 05 11:01:53 2014 +0200
@@ -76,7 +76,7 @@
 val presburger_ss = simpset_of (@{context} addsimps [zdvd1_eq]);
 val lin_ss =
   simpset_of (put_simpset presburger_ss @{context}
-    addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms add_ac [where 'a=int]}));
+    addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms ac_simps [where 'a=int]}));
 
 val iT = HOLogic.intT
 val bT = HOLogic.boolT;
@@ -826,7 +826,7 @@
     @ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
        @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
        @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
-    @ @{thms add_ac}
+    @ @{thms ac_simps}
    addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
 val splits_ss =
   simpset_of (put_simpset comp_ss @{context}
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Tools/group_cancel.ML
--- a/src/HOL/Tools/group_cancel.ML	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/group_cancel.ML	Sat Jul 05 11:01:53 2014 +0200
@@ -19,13 +19,13 @@
 struct
 
 val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
-      by (simp only: add_ac)}
+      by (simp only: ac_simps)}
 val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
-      by (simp only: add_ac)}
+      by (simp only: ac_simps)}
 val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
       by (simp only: add_diff_eq)}
 val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
-      by (simp only: minus_add diff_conv_add_uminus add_ac)}
+      by (simp only: minus_add diff_conv_add_uminus ac_simps)}
 val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
       by (simp only: minus_add_distrib)}
 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Sat Jul 05 11:01:53 2014 +0200
@@ -16,9 +16,9 @@
 struct
 
 val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
-      by (simp only: add_ac)}
+      by (simp only: ac_simps)}
 val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
-      by (simp only: add_ac)}
+      by (simp only: ac_simps)}
 val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
       by (simp only: add_Suc_right)}
 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Jul 05 11:01:53 2014 +0200
@@ -167,10 +167,10 @@
   val norm_ss1 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
       addsimps numeral_syms @ add_0s @ mult_1s @
-        [@{thm Suc_eq_plus1_left}] @ @{thms add_ac})
+        [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})
   val norm_ss2 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
-      addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
+      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
   fun norm_tac ctxt = 
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -239,10 +239,10 @@
 
   val norm_ss1 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
-      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac})
+      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms ac_simps})
   val norm_ss2 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
-      addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
+      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -270,10 +270,10 @@
 
   val norm_ss1 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
-      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac})
+      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})
   val norm_ss2 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
-      addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
+      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -363,7 +363,7 @@
   val trans_tac = Numeral_Simprocs.trans_tac
   val norm_ss =
     simpset_of (put_simpset HOL_basic_ss @{context}
-      addsimps mult_1s @ @{thms mult_ac})
+      addsimps mult_1s @ @{thms ac_simps})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   val simplify_meta_eq  = cancel_simplify_meta_eq
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Jul 05 11:01:53 2014 +0200
@@ -232,7 +232,7 @@
 val norm_ss1 =
   simpset_of (put_simpset num_ss @{context}
     addsimps numeral_syms @ add_0s @ mult_1s @
-    diff_simps @ minus_simps @ @{thms add_ac})
+    diff_simps @ minus_simps @ @{thms ac_simps})
 
 val norm_ss2 =
   simpset_of (put_simpset num_ss @{context}
@@ -240,7 +240,7 @@
 
 val norm_ss3 =
   simpset_of (put_simpset num_ss @{context}
-    addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac minus_mult_commute})
+    addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute})
 
 structure CancelNumeralsCommon =
 struct
@@ -361,7 +361,7 @@
 
 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
 struct
-  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
+  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
   val eq_reflection = eq_reflection
   val is_numeral = can HOLogic.dest_number
 end;
@@ -381,7 +381,7 @@
   val norm_ss2 =
     simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
   val norm_ss3 =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
+    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -513,7 +513,7 @@
   val find_first = find_first_t []
   val trans_tac = trans_tac
   val norm_ss =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac minus_mult_commute})
+    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms ac_simps minus_mult_commute})
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Transcendental.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -481,10 +481,10 @@
   apply (rule setsum.cong [OF refl])
   apply (simp add: less_iff_Suc_add)
   apply (clarify)
-  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
+  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
               del: setsum_lessThan_Suc power_Suc)
   apply (subst mult.assoc [symmetric], subst power_add [symmetric])
-  apply (simp add: mult_ac)
+  apply (simp add: ac_simps)
   done
 
 lemma real_setsum_nat_ivl_bounded2:
@@ -958,7 +958,7 @@
     hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
       by (rule order_trans [OF norm_mult_ineq])
     hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
-      by (simp add: pos_divide_le_eq mult_ac)
+      by (simp add: pos_divide_le_eq ac_simps)
     thus "norm (S (Suc n)) \<le> r * norm (S n)"
       by (simp add: S_Suc inverse_eq_divide)
   qed
@@ -1058,7 +1058,7 @@
     by (rule distrib_right)
   also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
                 + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
-    by (simp only: setsum_right_distrib mult_ac)
+    by (simp only: setsum_right_distrib ac_simps)
   also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
                 + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
     by (simp add: times_S Suc_diff_le)
@@ -1431,7 +1431,7 @@
       by (rule mult_mono)
         (rule mult_mono, simp_all add: power_le_one a b)
     hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
-      unfolding power_add by (simp add: mult_ac del: fact_Suc) }
+      unfolding power_add by (simp add: ac_simps del: fact_Suc) }
   note aux1 = this
   have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
     by (intro sums_mult geometric_sums, simp)
@@ -2476,7 +2476,7 @@
 proof -
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
     by (rule sin_converges [THEN sums_group], simp)
-  thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
+  thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
 qed
 
 lemma sin_gt_zero:
@@ -2512,7 +2512,7 @@
 proof -
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
     by (rule cos_converges [THEN sums_group], simp)
-  thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
+  thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
 qed
 
 lemmas realpow_num_eq_if = power_eq_if
@@ -2533,7 +2533,7 @@
 apply (drule sums_summable)
 apply simp
 apply (erule suminf_pos)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma cos_two_less_zero [simp]:
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -39,7 +39,7 @@
 (** bag_of **)
 
 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
-  by (induct l) (simp_all add: add_ac)
+  by (induct l) (simp_all add: ac_simps)
 
 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
 apply (rule monoI)
@@ -63,7 +63,7 @@
       (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
 apply (rule_tac xs = l in rev_induct, simp)
 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
-                 bag_of_sublist_lemma add_ac)
+                 bag_of_sublist_lemma ac_simps)
 done
 
 
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -783,7 +783,7 @@
   apply (case_tac binb rule: bin_exhaust)
   apply (case_tac b)
    apply (case_tac [!] "ba")
-     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def add_ac)
+     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
   done
 
 lemma rbl_add_app2: 
@@ -1021,7 +1021,7 @@
    apply (erule allE)
    apply (erule (1) impE)
    apply (drule bin_nth_split, erule conjE, erule allE,
-          erule trans, simp add : add_ac)+
+          erule trans, simp add : ac_simps)+
   done
 
 lemma bin_rsplit_all:
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Word/Word.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1592,7 +1592,7 @@
 lemma no_olen_add':
   fixes x :: "'a::len0 word"
   shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
-  by (simp add: add_ac no_olen_add)
+  by (simp add: ac_simps no_olen_add)
 
 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
 
@@ -1906,7 +1906,7 @@
 
 lemma Abs_fnat_hom_Suc:
   "word_succ (of_nat a) = of_nat (Suc a)"
-  by (simp add: word_of_nat wi_hom_succ add_ac)
+  by (simp add: word_of_nat wi_hom_succ ac_simps)
 
 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
   by simp
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -331,7 +331,7 @@
    prefer 2
    apply (erule asm_rl)
   apply (rule_tac f="%n. n div f" in arg_cong)
-  apply (simp add : mult_ac)
+  apply (simp add : ac_simps)
   done
     
 lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Sat Jul 05 11:01:53 2014 +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: distrib_right [symmetric] divide_inverse mult_ac
+      by (simp add: distrib_right [symmetric] divide_inverse ac_simps
           order_less_imp_not_eq2)
   next
     show "y * ?f \<in> B"
@@ -326,7 +326,7 @@
 
 lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
 apply (simp add: preal_add_def mem_add_set Rep_preal)
-apply (force simp add: add_set_def add_ac)
+apply (force simp add: add_set_def ac_simps)
 done
 
 instance preal :: ab_semigroup_add
@@ -454,7 +454,7 @@
 
 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
 apply (simp add: preal_mult_def mem_mult_set Rep_preal)
-apply (force simp add: mult_set_def mult_ac)
+apply (force simp add: mult_set_def ac_simps)
 done
 
 instance preal :: ab_semigroup_mult
@@ -713,7 +713,7 @@
   have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
   proof -
     have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
-      by (simp add: order_less_imp_not_eq2 mult_ac) 
+      by (simp add: order_less_imp_not_eq2 ac_simps) 
     moreover
     have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
       by (rule mult_mono, 
@@ -961,7 +961,7 @@
 apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
 apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)  
 apply (rule_tac x="y+xa" in exI) 
-apply (auto simp add: add_ac)
+apply (auto simp add: ac_simps)
 done
 
 lemma mem_diff_set:
@@ -1032,7 +1032,7 @@
   proof (intro exI conjI)
     show "r \<in> Rep_preal R" by (rule r)
     show "r + e \<notin> Rep_preal R" by (rule notin)
-    show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
+    show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: ac_simps)
     show "x = r + y" by (simp add: eq)
     show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
       by simp
@@ -1236,11 +1236,11 @@
     and "x + y2 = x2 + y"
   shows "x1 + y2 = x2 + (y1::preal)"
 proof -
-  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
+  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: ac_simps)
   also have "... = (x2 + y) + x1"  by (simp add: assms)
-  also have "... = x2 + (x1 + y)"  by (simp add: add_ac)
+  also have "... = x2 + (x1 + y)"  by (simp add: ac_simps)
   also have "... = x2 + (x + y1)"  by (simp add: assms)
-  also have "... = (x2 + y1) + x"  by (simp add: add_ac)
+  also have "... = (x2 + y1) + x"  by (simp add: ac_simps)
   finally have "(x1 + y2) + x = (x2 + y1) + x" .
   thus ?thesis by (rule add_right_imp_eq)
 qed
@@ -1287,7 +1287,7 @@
 apply (simp add: add.assoc)
 apply (rule add.left_commute [of ab, THEN ssubst])
 apply (simp add: add.assoc [symmetric])
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma real_add:
@@ -1318,7 +1318,7 @@
   show "x + y = y + x"
     by (cases x, cases y, simp add: real_add add.commute)
   show "0 + x = x"
-    by (cases x, simp add: real_add real_zero_def add_ac)
+    by (cases x, simp add: real_add real_zero_def ac_simps)
   show "- x + x = 0"
     by (cases x, simp add: real_minus real_add real_zero_def add.commute)
   show "x - y = x + - y"
@@ -1354,7 +1354,7 @@
          UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2])
 
 lemma real_mult_commute: "(z::real) * w = w * z"
-by (cases z, cases w, simp add: real_mult add_ac mult_ac)
+by (cases z, cases w, simp add: real_mult ac_simps ac_simps)
 
 lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
 apply (cases z1, cases z2, cases z3)
@@ -1456,7 +1456,7 @@
   shows "x1 + y2 \<le> x2 + (y1::preal)"
 proof -
   have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: assms)
-  hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac)
+  hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: ac_simps)
   also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: assms)
   finally show ?thesis by simp
 qed
@@ -1477,10 +1477,10 @@
     and "x2 + v2 = u2 + y2"
   shows "x + v' \<le> u' + (y::preal)"
 proof -
-  have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac)
+  have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: ac_simps)
   also have "... \<le> (u+y) + (u+v')" by (simp add: assms)
   also have "... \<le> (u+y) + (u'+v)" by (simp add: assms)
-  also have "... = (u'+y) + (u+v)"  by (simp add: add_ac)
+  also have "... = (u'+y) + (u+v)"  by (simp add: ac_simps)
   finally show ?thesis by simp
 qed
 
@@ -1500,7 +1500,7 @@
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
 apply (cases z, cases w)
-apply (auto simp add: real_le real_zero_def add_ac)
+apply (auto simp add: real_le real_zero_def ac_simps)
 done
 
 instance real :: linorder
@@ -1509,7 +1509,7 @@
 lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
 apply (cases x, cases y) 
 apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
-                      add_ac)
+                      ac_simps)
 apply (simp_all add: add.assoc [symmetric])
 done
 
@@ -1589,7 +1589,7 @@
 lemma real_of_preal_trichotomy:
       "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
 apply (simp add: real_of_preal_def real_zero_def, cases x)
-apply (auto simp add: real_minus add_ac)
+apply (auto simp add: real_minus ac_simps)
 apply (cut_tac x = xa and y = y in linorder_less_linear)
 apply (auto dest!: less_add_left_Ex simp add: add.assoc [symmetric])
 done
@@ -1616,9 +1616,9 @@
 lemma real_of_preal_zero_less: "0 < real_of_preal m"
 apply (insert preal_self_less_add_left [of 1 m])
 apply (auto simp add: real_zero_def real_of_preal_def
-                      real_less_def real_le_def add_ac)
+                      real_less_def real_le_def ac_simps)
 apply (rule_tac x="m + 1" in exI, rule_tac x="1" in exI)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
 done
 
 lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/ex/Sqrt.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -33,7 +33,7 @@
     from eq have "p dvd m\<^sup>2" ..
     with `prime p` show "p dvd m" by (rule prime_dvd_power_nat)
     then obtain k where "m = p * k" ..
-    with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
+    with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
     with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
     then have "p dvd n\<^sup>2" ..
     with `prime p` show "p dvd n" by (rule prime_dvd_power_nat)
@@ -73,7 +73,7 @@
   then have "p dvd m\<^sup>2" ..
   with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
   then obtain k where "m = p * k" ..
-  with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
+  with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
   with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
   then have "p dvd n\<^sup>2" ..
   with `prime p` have "p dvd n" by (rule prime_dvd_power_nat)
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/ex/Sqrt_Script.thy
--- a/src/HOL/ex/Sqrt_Script.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -36,7 +36,7 @@
   done
 
 lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"
-  by (simp add: mult_ac)
+  by (simp add: ac_simps)
 
 lemma prime_not_square:
     "prime (p::nat) \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/ex/ThreeDivides.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -80,7 +80,7 @@
   hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
   ultimately
   have"?thr dvd ((10^(n+1) - 10) + 9)"
-    by (simp only: add_ac) (rule dvd_add)
+    by (simp only: ac_simps) (rule dvd_add)
   thus ?case by simp
 qed
 
@@ -194,7 +194,7 @@
       "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
     also have
       "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
-      by (subst setsum_right_distrib) (simp add: mult_ac)
+      by (subst setsum_right_distrib) (simp add: ac_simps)
     also have
       "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
       by (simp add: div_mult2_eq[symmetric])