changeset 13758 | ee898d32de21 |
parent 11866 | fbd097aec213 |
child 13778 | 61272514e3b5 |
--- a/doc-src/TutorialI/Misc/document/Option2.tex Tue Dec 17 11:04:58 2002 +0100 +++ b/doc-src/TutorialI/Misc/document/Option2.tex Tue Dec 17 11:05:41 2002 +0100 @@ -26,6 +26,7 @@ \S\ref{sec:Trie}.% \end{isamarkuptext}% \isamarkuptrue% +\isanewline \isamarkupfalse% \end{isabellebody}% %%% Local Variables: