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