1.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:18 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:24 2000 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \label{sec:rtc}
     1.7 +
     1.8  {\bf Say something about inductive relations as opposed to sets? Or has that
     1.9  been said already? If not, explain induction!}
    1.10  
    1.11 @@ -13,7 +14,7 @@
    1.12  closure of a relation. This concept was already introduced in
    1.13  \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
    1.14  the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
    1.15 -fixed point because at that point in the theory hierarchy
    1.16 +fixpoint because at that point in the theory hierarchy
    1.17  inductive definitions are not yet available. But now they are:%
    1.18  \end{isamarkuptext}%
    1.19  \isacommand{consts}\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
    1.20 @@ -26,9 +27,8 @@
    1.21  The function \isa{rtc} is annotated with concrete syntax: instead of
    1.22  \isa{rtc\ r} we can read and write {term"r*"}. The actual definition
    1.23  consists of two rules. Reflexivity is obvious and is immediately declared an
    1.24 -equivalence rule.  Thus the automatic tools will apply it automatically. The
    1.25 -second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more
    1.26 -\isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
    1.27 +equivalence.  Thus the automatic tools will apply it automatically. The second
    1.28 +rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more \isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
    1.29  introduction rule, this is dangerous: the recursion slows down and may
    1.30  even kill the automatic tactics.
    1.31