# HG changeset patch
# User wenzelm
# Date 1004043506 -7200
# Node ID ff966c79cfbc0bffb805fd726a69498ab27aeaa2
# Parent  80365073b8b31ea5d5ec38bda9ee20c287e5e1f1
updated;

diff -r 80365073b8b3 -r ff966c79cfbc doc-src/TutorialI/Types/document/Typedefs.tex
--- 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%