--- a/doc-src/TutorialI/Datatype/document/Nested.tex Mon Oct 09 17:40:47 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Mon Oct 09 19:20:55 2000 +0200
@@ -75,10 +75,10 @@
The fact that substitution distributes over composition can be expressed
roughly as follows:
\begin{isabelle}%
-\ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
+\ \ \ \ \ subst\ {\isacharparenleft}f\ {\isasymcirc}\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
\end{isabelle}
Correct this statement (you will find that it does not type-check),
-strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
+strengthen it, and prove it. (Note: \isa{{\isasymcirc}} is function composition;
its definition is found in theorem \isa{o{\isacharunderscore}def}).
\end{exercise}
\begin{exercise}\label{ex:trev-trev}