--- a/doc-src/TutorialI/Types/document/Typedefs.tex Thu Oct 25 22:43:58 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex Thu Oct 25 22:58:26 2001 +0200
@@ -227,7 +227,7 @@
\isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ numerals{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ numerals{\isacharparenright}\ \ \ \isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}{\isacharparenleft}erule\ le{\isacharunderscore}SucE{\isacharparenright}{\isacharplus}{\isacharparenright}\isanewline
\isamarkupfalse%