1.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Fri May 18 12:13:53 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Fri May 18 16:45:55 2001 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  The rest of this section is devoted to proving that it is equivalent to
     1.5  the standard definition. We start with a simple lemma:%
     1.6  \end{isamarkuptext}%
     1.7 -\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
     1.8 +\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
     1.9  \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
    1.10  \begin{isamarkuptext}%
    1.11  \noindent