changeset 9722 | a5f86aed785b |
parent 9721 | 7e51c9f3d5a0 |
child 9754 | a123a64cadeb |
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 15:13:10 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 15:43:29 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"