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.