diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Sun Aug 06 15:26:53 2000 +0200
@@ -7,10 +7,10 @@
 \isa{rev} reqires an extra argument where the result is accumulated
 gradually, using only \isa{\#}:%
 \end{isamarkuptext}%
-\isacommand{consts}~itrev~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
+\isacommand{consts}\ itrev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
 \isacommand{primrec}\isanewline
-{"}itrev~[]~~~~~ys~=~ys{"}\isanewline
-{"}itrev~(x\#xs)~ys~=~itrev~xs~(x\#ys){"}%
+{"}itrev\ []\ \ \ \ \ ys\ =\ ys{"}\isanewline
+{"}itrev\ (x\#xs)\ ys\ =\ itrev\ xs\ (x\#ys){"}%
 \begin{isamarkuptext}%
 \noindent The behaviour of \isa{itrev} is simple: it reverses
 its first argument by stacking its elements onto the second argument,
@@ -21,12 +21,12 @@
 Naturally, we would like to show that \isa{itrev} does indeed reverse
 its first argument provided the second one is empty:%
 \end{isamarkuptext}%
-\isacommand{lemma}~{"}itrev~xs~[]~=~rev~xs{"}%
+\isacommand{lemma}\ {"}itrev\ xs\ []\ =\ rev\ xs{"}%
 \begin{isamarkuptxt}%
 \noindent
 There is no choice as to the induction variable, and we immediately simplify:%
 \end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~xs,~auto)%
+\isacommand{apply}(induct\_tac\ xs,\ auto)%
 \begin{isamarkuptxt}%
 \noindent
 Unfortunately, this is not a complete success:
@@ -43,11 +43,11 @@
 Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
 just not true---the correct generalization is%
 \end{isamarkuptxt}%
-\isacommand{lemma}~{"}itrev~xs~ys~=~rev~xs~@~ys{"}%
+\isacommand{lemma}\ {"}itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}%
 \begin{isamarkuptxt}%
 \noindent
 If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
-\isa{rev xs}, just as required.
+\isa{rev\ xs}, just as required.
 
 In this particular instance it was easy to guess the right generalization,
 but in more complex situations a good deal of creativity is needed. This is
@@ -64,10 +64,10 @@
 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
-\isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem
+\isa{a\ \#\ ys} instead of \isa{ys}. Hence we prove the theorem
 for all \isa{ys} instead of a fixed one:%
 \end{isamarkuptxt}%
-\isacommand{lemma}~{"}{\isasymforall}ys.~itrev~xs~ys~=~rev~xs~@~ys{"}%
+\isacommand{lemma}\ {"}{\isasymforall}ys.\ itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}%
 \begin{isamarkuptxt}%
 \noindent
 This time induction on \isa{xs} followed by simplification succeeds. This