diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/examples.tex --- a/doc-src/TutorialI/Recdef/document/examples.tex Tue Aug 29 11:52:47 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Aug 29 12:08:20 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% Here is a simple example, the Fibonacci function:% @@ -77,7 +78,7 @@ For non-recursive functions the termination measure degenerates to the empty set \isa{\{\}}.% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root"