diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/Nested0.tex --- 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"