doc-src/TutorialI/Recdef/document/termination.tex
changeset 16069 3f2a9f400168
parent 15481 fc075ae929e4
child 17056 05fc32a23b8b
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Wed May 25 09:03:53 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Wed May 25 09:04:24 2005 +0200
@@ -65,8 +65,9 @@
 \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%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent