diff -r 93d5408eb7d9 -r fbd097aec213 doc-src/TutorialI/Misc/document/appendix.tex --- a/doc-src/TutorialI/Misc/document/appendix.tex Sun Oct 21 19:48:19 2001 +0200 +++ b/doc-src/TutorialI/Misc/document/appendix.tex Sun Oct 21 19:49:29 2001 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{appendix}% +\isamarkupfalse% % \begin{isamarkuptext}% \begin{table}[htbp] @@ -31,6 +32,8 @@ \end{center} \end{table}% \end{isamarkuptext}% +\isamarkuptrue% +\isamarkupfalse% \end{isabellebody}% %%% Local Variables: %%% mode: latex