1.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Tue Aug 29 15:43:29 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Tue Aug 29 16:05:13 2000 +0200
     1.3 @@ -32,9 +32,9 @@
     1.4  
     1.5  txt{*\noindent
     1.6  Unfortunately, this is not a complete success:
     1.7 -\begin{isabellepar}%
     1.8 +\begin{isabelle}
     1.9  ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
    1.10 -\end{isabellepar}%
    1.11 +\end{isabelle}
    1.12  Just as predicted above, the overall goal, and hence the induction
    1.13  hypothesis, is too weak to solve the induction step because of the fixed
    1.14  \isa{[]}. The corresponding heuristic:
    1.15 @@ -59,11 +59,11 @@
    1.16  Although we now have two variables, only \isa{xs} is suitable for
    1.17  induction, and we repeat our above proof attempt. Unfortunately, we are still
    1.18  not there:
    1.19 -\begin{isabellepar}%
    1.20 +\begin{isabelle}
    1.21  ~1.~{\isasymAnd}a~list.\isanewline
    1.22  ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
    1.23  ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
    1.24 -\end{isabellepar}%
    1.25 +\end{isabelle}
    1.26  The induction hypothesis is still too weak, but this time it takes no
    1.27  intuition to generalize: the problem is that \isa{ys} is fixed throughout
    1.28  the subgoal, but the induction hypothesis needs to be applied with