diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/Nested0.tex --- a/doc-src/TutorialI/Recdef/document/Nested0.tex Mon Sep 11 17:59:53 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Mon Sep 11 18:00:47 2000 +0200 @@ -1,5 +1,6 @@ % \begin{isabellebody}% +\def\isabellecontext{Nested0}% % \begin{isamarkuptext}% In \S\ref{sec:nested-datatype} we defined the datatype of terms%