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