doc-src/TutorialI/Recdef/document/Nested2.tex
changeset 9722 a5f86aed785b
parent 9721 7e51c9f3d5a0
child 9754 a123a64cadeb
     1.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Aug 29 15:13:10 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Aug 29 15:43:29 2000 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4 -\begin{isabelle}%
     1.5 +%
     1.6 +\begin{isabellebody}%
     1.7  %
     1.8  \begin{isamarkuptext}%
     1.9  \noindent
    1.10 @@ -90,7 +91,7 @@
    1.11  declaring a congruence rule for the simplifier does not make it
    1.12  available to \isacommand{recdef}, and vice versa. This is intentional.%
    1.13  \end{isamarkuptext}%
    1.14 -\end{isabelle}%
    1.15 +\end{isabellebody}%
    1.16  %%% Local Variables:
    1.17  %%% mode: latex
    1.18  %%% TeX-master: "root"