--- a/doc-src/TutorialI/Recdef/document/termination.tex Sun Jan 30 20:48:50 2005 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Feb 01 18:01:57 2005 +0100
@@ -65,9 +65,8 @@
\isamarkuptrue%
\isacommand{theorem}\ {\isachardoublequote}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
+\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent