
diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -31,7 +31,7 @@
 It was not proved automatically because of the special nature of \isa{-}
 on \isa{nat}. This requires more arithmetic than is tried by default:%
 \end{isamarkuptxt}%
-\isacommand{apply}(arith)\isacommand{.}%
+\isacommand{by}(arith)%
 \begin{isamarkuptext}%
 \noindent
 Because \isacommand{recdef}'s termination prover involves simplification,
@@ -48,7 +48,7 @@
 rules. Thus we can automatically prove%
 \end{isamarkuptext}%
 \isacommand{theorem}~wow:~{"}g(1,0)~=~g(1,1){"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}%
+\isacommand{by}(simp)%
 \begin{isamarkuptext}%
 \noindent
 More exciting theorems require induction, which is discussed below.




