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}