changeset 13758 | ee898d32de21 |
parent 11866 | fbd097aec213 |
child 13778 | 61272514e3b5 |
--- a/doc-src/TutorialI/Misc/document/pairs.tex Tue Dec 17 11:04:58 2002 +0100 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Tue Dec 17 11:05:41 2002 +0100 @@ -33,6 +33,7 @@ For more information on pairs and records see Chapter~\ref{ch:more-types}.% \end{isamarkuptext}% \isamarkuptrue% +\isanewline \isamarkupfalse% \end{isabellebody}% %%% Local Variables: