--- a/doc-src/TutorialI/Misc/document/Itrev.tex Wed Dec 27 18:26:32 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Dec 27 18:26:53 2000 +0100
@@ -62,7 +62,8 @@
Unfortunately, this is not a complete success:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
-\ \ \ \ \ \ \ itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
+\ \ \ \ \ \ \ itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ \ \ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
\end{isabelle}
Just as predicted above, the overall goal, and hence the induction
hypothesis, is too weak to solve the induction step because of the fixed