diff -r 891fbd3f4881 -r b28bbb153603 doc-src/TutorialI/Inductive/document/Star.tex
--- a/doc-src/TutorialI/Inductive/document/Star.tex	Fri May 18 12:13:53 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Fri May 18 16:45:55 2001 +0200
@@ -38,7 +38,7 @@
 The rest of this section is devoted to proving that it is equivalent to
 the standard definition. We start with a simple lemma:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent