diff -r de51a86fc903 -r cc97b347b301 src/Doc/Tutorial/document/rules.tex
--- a/src/Doc/Tutorial/document/rules.tex	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/Doc/Tutorial/document/rules.tex	Fri Jul 04 20:18:47 2014 +0200
@@ -751,11 +751,11 @@
 Now we wish to apply a commutative law:
 \begin{isabelle}
 ?m\ *\ ?n\ =\ ?n\ *\ ?m%
-\rulename{mult_commute}
+\rulename{mult.commute}
 \end{isabelle}
 Isabelle rejects our first attempt:
 \begin{isabelle}
-apply (simp add: mult_commute)
+apply (simp add: mult.commute)
 \end{isabelle}
 The simplifier notices the danger of looping and refuses to apply the
 rule.%
@@ -764,9 +764,9 @@
 is already smaller than
 \isa{y\ *\ x}.}
 %
-The \isa{subst} method applies \isa{mult_commute} exactly once.  
+The \isa{subst} method applies \isa{mult.commute} exactly once.  
 \begin{isabelle}
-\isacommand{apply}\ (subst\ mult_commute)\isanewline
+\isacommand{apply}\ (subst\ mult.commute)\isanewline
 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \
 \isasymLongrightarrow \ f\ z\ =\ y\ *\ x%
 \end{isabelle}
@@ -775,7 +775,7 @@
 \medskip
 This use of the \methdx{subst} method has the same effect as the command
 \begin{isabelle}
-\isacommand{apply}\ (rule\ mult_commute [THEN ssubst])
+\isacommand{apply}\ (rule\ mult.commute [THEN ssubst])
 \end{isabelle}
 The attribute \isa{THEN}, which combines two rules, is described in 
 {\S}\ref{sec:THEN} below. The \methdx{subst} method is more powerful than
@@ -1986,9 +1986,9 @@
 %  exercise worth including? E.g. find a difference between the two ways
 %  of substituting.
 %\begin{exercise}
-%In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied.  How
+%In {\S}\ref{sec:subst} the method \isa{subst\ mult.commute} was applied.  How
 %can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
-%% answer  rule (mult_commute [THEN ssubst])
+%% answer  rule (mult.commute [THEN ssubst])
 %\end{exercise}
 
 \subsection{Modifying a Theorem using {\tt\slshape OF}}