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