diff -r de51a86fc903 -r cc97b347b301 src/Doc/Tutorial/Rules/Basic.thy
--- a/src/Doc/Tutorial/Rules/Basic.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/Doc/Tutorial/Rules/Basic.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -64,11 +64,11 @@
 text {*
 the subst method
 
-@{thm[display] mult_commute}
-\rulename{mult_commute}
+@{thm[display] mult.commute}
+\rulename{mult.commute}
 
 this would fail:
-apply (simp add: mult_commute) 
+apply (simp add: mult.commute) 
 *}
 
 
@@ -76,7 +76,7 @@
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 *}
-apply (subst mult_commute) 
+apply (subst mult.commute) 
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 *}
@@ -84,7 +84,7 @@
 
 (*exercise involving THEN*)
 lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y"
-apply (rule mult_commute [THEN ssubst]) 
+apply (rule mult.commute [THEN ssubst]) 
 oops