--- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
%
\begin{isamarkuptext}%
So far, all datatypes had the property that on the right-hand side of their
@@ -121,7 +122,7 @@
constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
expressions as its argument: \isa{Sum "'a aexp list"}.%
\end{isamarkuptext}%
-\end{isabelle}%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"