diff -r 2f5edb146f7e -r 1f073030b97a doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Fri Jan 18 18:30:19 2002 +0100
@@ -20,7 +20,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}\ trev{\isachardot}induct{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \begin{isabelle}%
@@ -32,7 +32,7 @@
 Both the base case and the induction step fall to simplification:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent