diff -r 00fdd5c330ea -r a72ddfdbfca0 doc-src/TutorialI/CTL/document/PDL.tex
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Fri Oct 06 01:21:17 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Fri Oct 06 12:31:53 2000 +0200
@@ -73,7 +73,8 @@
 \end{isamarkuptext}%
 \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
+\isacommand{apply}\ blast\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 in order to make sure it really has a least fixpoint.
@@ -163,14 +164,16 @@
 The proof of the induction step is identical to the one for the base case:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 The main theorem is proved in the familiar manner: induction followed by
 \isa{auto} augmented with the lemma as a simplification rule.%
 \end{isamarkuptext}%
 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\end{isabellebody}%
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
+\isacommand{done}\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"