diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/termination.thy
--- a/doc-src/TutorialI/Recdef/termination.thy	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Jul 28 16:02:51 2000 +0200
@@ -36,7 +36,7 @@
 on \isa{nat}. This requires more arithmetic than is tried by default:
 *}
 
-apply(arith).;
+by(arith);
 
 text{*\noindent
 Because \isacommand{recdef}'s termination prover involves simplification,
@@ -55,7 +55,7 @@
 *}
 
 theorem wow: "g(1,0) = g(1,1)";
-apply(simp).;
+by(simp);
 
 text{*\noindent
 More exciting theorems require induction, which is discussed below.