changeset 13758 | ee898d32de21 |
parent 12699 | deae80045527 |
child 13778 | 61272514e3b5 |
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Dec 17 11:04:58 2002 +0100 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Dec 17 11:05:41 2002 +0100 @@ -103,6 +103,7 @@ \end{warn}% \end{isamarkuptext}% \isamarkuptrue% +\isanewline \isamarkupfalse% \end{isabellebody}% %%% Local Variables: