changeset 9719 | c753196599f9 |
parent 9698 | f0740137a65d |
child 9721 | 7e51c9f3d5a0 |
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 11:52:47 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 12:08:20 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% In \S\ref{sec:nested-datatype} we defined the datatype of terms% @@ -16,7 +17,7 @@ FIXME: declare trev now!% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root"