doc-src/TutorialI/Recdef/document/Nested0.tex
changeset 10267 325ead6d9457
parent 10186 499637e8f2c6
child 10878 b254d5ad6dd4
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Oct 18 23:44:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Oct 18 23:58:07 2000 +0200
@@ -1,6 +1,6 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{Nested0}%
+\def\isabellecontext{Nested{\isadigit{0}}}%
 %
 \begin{isamarkuptext}%
 In \S\ref{sec:nested-datatype} we defined the datatype of terms%