--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Sun Aug 28 19:42:10 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Sun Aug 28 19:42:19 2005 +0200
@@ -7,6 +7,7 @@
\endisadelimtheory
%
\isatagtheory
+\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
@@ -14,7 +15,6 @@
\isadelimtheory
%
\endisadelimtheory
-\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent
@@ -27,11 +27,11 @@
simplifies matters because we are now free to use the recursion equation
suggested at the end of \S\ref{sec:nested-datatype}:%
\end{isamarkuptext}%
-\isamarkupfalse%
-\isacommand{recdef}\ trev\ {\isachardoublequote}measure\ size{\isachardoublequote}\isanewline
-\ {\isachardoublequote}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ Var\ x{\isachardoublequote}\isanewline
-\ {\isachardoublequote}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}rev{\isacharparenleft}map\ trev\ ts{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
-%
+\isamarkuptrue%
+\isacommand{recdef}\isamarkupfalse%
+\ trev\ {\isachardoublequoteopen}measure\ size{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ Var\ x{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}rev{\isacharparenleft}map\ trev\ ts{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
Remember that function \isa{size} is defined for each \isacommand{datatype}.
@@ -55,12 +55,14 @@
The termination condition is easily proved by induction:%
\end{isamarkuptext}%
+\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
+\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%