1.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Fri Feb 16 00:36:21 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Fri Feb 16 06:46:20 2001 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  Relations too can be defined inductively, since they are just sets of pairs.
     1.5  A perfect example is the function that maps a relation to its
     1.6  reflexive transitive closure.  This concept was already
     1.7 -introduced in \S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was
     1.8 +introduced in \S\ref{sec:Relations}, where the operator \isa{\isactrlsup {\isacharasterisk}} was
     1.9  defined as a least fixed point because inductive definitions were not yet
    1.10  available. But now they are:%
    1.11  \end{isamarkuptext}%
    1.12 @@ -102,7 +102,7 @@
    1.13  \end{quote}
    1.14  A similar heuristic for other kinds of inductions is formulated in
    1.15  \S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns
    1.16 -\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}. Thus in the end we obtain the original
    1.17 +\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original
    1.18  statement of our lemma.%
    1.19  \end{isamarkuptxt}%
    1.20  \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
    1.21 @@ -152,8 +152,7 @@
    1.22  contains only two rules, and the single step rule is simpler than
    1.23  transitivity.  As a consequence, \isa{rtc{\isachardot}induct} is simpler than
    1.24  \isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough
    1.25 -anyway, we should
    1.26 -certainly pick the simplest induction schema available.
    1.27 +anyway, we should always pick the simplest induction schema available.
    1.28  Hence \isa{rtc} is the definition of choice.
    1.29  
    1.30  \begin{exercise}\label{ex:converse-rtc-step}