doc-src/TutorialI/Types/document/Numbers.tex
changeset 38767 d8da44a8dd25
parent 37216 3165bc303f66
child 40406 313a24b66a8d
     1.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Fri Aug 27 00:09:56 2010 +0200
     1.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Fri Aug 27 12:40:20 2010 +0200
     1.3 @@ -26,16 +26,16 @@
     1.4  %
     1.5  \isatagML
     1.6  \isacommand{ML}\isamarkupfalse%
     1.7 -\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
     1.8 -\isacommand{ML}\isamarkupfalse%
     1.9 -\ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
    1.10 +\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}%
    1.11  \endisatagML
    1.12  {\isafoldML}%
    1.13  %
    1.14  \isadelimML
    1.15 +\isanewline
    1.16  %
    1.17  \endisadelimML
    1.18 -%
    1.19 +\isacommand{declare}\isamarkupfalse%
    1.20 +\ {\isacharbrackleft}{\isacharbrackleft}thy{\isacharunderscore}output{\isacharunderscore}indent\ {\isacharequal}\ {\isadigit{0}}{\isacharbrackright}{\isacharbrackright}%
    1.21  \begin{isamarkuptext}%
    1.22  numeric literals; default simprules; can re-orient%
    1.23  \end{isamarkuptext}%