doc-src/TutorialI/Datatype/document/Nested.tex
changeset 28838 d5db6dfcb34a
parent 27319 6584901d694c
child 40685 313a24b66a8d
     1.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Nov 18 18:22:49 2008 +0100
     1.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Nov 18 18:25:10 2008 +0100
     1.3 @@ -119,7 +119,7 @@
     1.4  its definition is found in theorem \isa{o{\isacharunderscore}def}).
     1.5  \end{exercise}
     1.6  \begin{exercise}\label{ex:trev-trev}
     1.7 -  Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term}
     1.8 +  Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term}
     1.9  that recursively reverses the order of arguments of all function symbols in a
    1.10    term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
    1.11  \end{exercise}