1.1 --- a/doc-src/Tutorial/fp.tex	Tue Aug 22 10:59:15 2000 +0200
     1.2 +++ b/doc-src/Tutorial/fp.tex	Tue Aug 22 11:24:24 2000 +0200
     1.3 @@ -1079,7 +1079,7 @@
     1.4  \ttbreak
     1.5  set trace_simp;
     1.6  by(Simp_tac 1);
     1.7 -\ttbreak\makeatother
     1.8 +\ttbreak
     1.9  \Out{ Applying instance of rewrite rule:}
    1.10  \Out{ rev (?x # ?xs) == rev ?xs @ [?x]}
    1.11  \Out{ Rewriting:}
    1.12 @@ -1089,7 +1089,7 @@
    1.13  \Out{ rev [] == []}
    1.14  \Out{ Rewriting:}
    1.15  \Out{ rev [] == []}
    1.16 -\ttbreak\makeatother
    1.17 +\ttbreak
    1.18  \Out{ Applying instance of rewrite rule:}
    1.19  \Out{ [] @ ?y == ?y}
    1.20  \Out{ Rewriting:}
    1.21 @@ -1158,8 +1158,8 @@
    1.22  \begin{ttbox}
    1.23  \input{Misc/itrev1.ML}\end{ttbox}
    1.24  There is no choice as to the induction variable, and we immediately simplify:
    1.25 -\begin{ttbox}
    1.26 -\input{Misc/induct_auto.ML}\ttbreak\makeatother
    1.27 +\begin{ttbox}\makeatother
    1.28 +\input{Misc/induct_auto.ML}\ttbreak
    1.29  \Out{ 1. !!a list. itrev list [] = rev list\(\;\)==> itrev list [a] = rev list @ [a]}
    1.30  \end{ttbox}
    1.31  Just as predicted above, the overall goal, and hence the induction