diff -r 11aa41ed306d -r 1eced27ee0e1 doc-src/TutorialI/Recdef/document/Nested1.tex --- 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}%