diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -79,9 +79,9 @@
 derived conditional ones. For \isa{gcd} it means we have to prove%
 \end{isamarkuptext}%
 \isacommand{lemma}~[simp]:~{"}gcd~(m,~0)~=~m{"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}\isanewline
+\isacommand{by}(simp)\isanewline
 \isacommand{lemma}~[simp]:~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~gcd(m,~n)~=~gcd(n,~m~mod~n){"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}%
+\isacommand{by}(simp)%
 \begin{isamarkuptext}%
 \noindent
 after which we can disable the original simplification rule:%