--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent Parameter \isa{'a} is the type of values stored in
@@ -50,7 +49,7 @@
~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
\end{isabellepar}%%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"