doc-src/TutorialI/Recdef/document/Nested2.tex
changeset 10267 325ead6d9457
parent 10212 33fe2d701ddd
child 10589 b2d1b393b750
     1.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Oct 18 23:44:52 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Oct 18 23:58:07 2000 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  %
     1.5  \begin{isabellebody}%
     1.6 -\def\isabellecontext{Nested2}%
     1.7 +\def\isabellecontext{Nested{\isadigit{2}}}%
     1.8  %
     1.9  \begin{isamarkuptext}%
    1.10  \noindent