diff -r 6e1f3d609a68 -r 403585a89772 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Sat May 08 16:53:53 2010 +0200 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Sat May 08 19:14:13 2010 +0200 @@ -26,7 +26,7 @@ % \isatagML \isacommand{ML}\isamarkupfalse% -\ {\isachardoublequoteopen}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline +\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline \isacommand{ML}\isamarkupfalse% \ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}% \endisatagML