--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Wed Oct 11 09:09:06 2000 +0200
@@ -1,7 +1,7 @@
%
\begin{isabellebody}%
\def\isabellecontext{Nested1}%
-\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
+%
\begin{isamarkuptext}%
\noindent
Although the definition of \isa{trev} is quite natural, we will have