--- 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