--- a/doc-src/TutorialI/Misc/Itrev.thy Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Tue Aug 29 16:05:13 2000 +0200
@@ -32,9 +32,9 @@
txt{*\noindent
Unfortunately, this is not a complete success:
-\begin{isabellepar}%
+\begin{isabelle}
~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
-\end{isabellepar}%
+\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
\isa{[]}. The corresponding heuristic:
@@ -59,11 +59,11 @@
Although we now have two variables, only \isa{xs} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
-\begin{isabellepar}%
+\begin{isabelle}
~1.~{\isasymAnd}a~list.\isanewline
~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
-\end{isabellepar}%
+\end{isabelle}
The induction hypothesis is still too weak, but this time it takes no
intuition to generalize: the problem is that \isa{ys} is fixed throughout
the subgoal, but the induction hypothesis needs to be applied with