1.1 --- a/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 18 17:19:18 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 18 17:19:24 2000 +0200
     1.3 @@ -3,6 +3,7 @@
     1.4  section{*The reflexive transitive closure*}
     1.5  
     1.6  text{*\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 @@ -24,9 +25,9 @@
    1.12  The function @{term rtc} is annotated with concrete syntax: instead of
    1.13  @{text"rtc r"} we can read and write {term"r*"}. The actual definition
    1.14  consists of two rules. Reflexivity is obvious and is immediately declared an
    1.15 -equivalence rule.  Thus the automatic tools will apply it automatically. The
    1.16 -second rule, @{thm[source]rtc_step}, says that we can always add one more
    1.17 -@{term r}-step to the left. Although we could make @{thm[source]rtc_step} an
    1.18 +equivalence.  Thus the automatic tools will apply it automatically. The second
    1.19 +rule, @{thm[source]rtc_step}, says that we can always add one more @{term
    1.20 +r}-step to the left. Although we could make @{thm[source]rtc_step} an
    1.21  introduction rule, this is dangerous: the recursion slows down and may
    1.22  even kill the automatic tactics.
    1.23  

     2.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:18 2000 +0200
     2.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:24 2000 +0200
     2.3 @@ -6,6 +6,7 @@
     2.4  %
     2.5  \begin{isamarkuptext}%
     2.6  \label{sec:rtc}
     2.7 +
     2.8  {\bf Say something about inductive relations as opposed to sets? Or has that
     2.9  been said already? If not, explain induction!}
    2.10  
    2.11 @@ -13,7 +14,7 @@
    2.12  closure of a relation. This concept was already introduced in
    2.13  \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
    2.14  the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
    2.15 -fixed point because at that point in the theory hierarchy
    2.16 +fixpoint because at that point in the theory hierarchy
    2.17  inductive definitions are not yet available. But now they are:%
    2.18  \end{isamarkuptext}%
    2.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
    2.20 @@ -26,9 +27,8 @@
    2.21  The function \isa{rtc} is annotated with concrete syntax: instead of
    2.22  \isa{rtc\ r} we can read and write {term"r*"}. The actual definition
    2.23  consists of two rules. Reflexivity is obvious and is immediately declared an
    2.24 -equivalence rule.  Thus the automatic tools will apply it automatically. The
    2.25 -second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more
    2.26 -\isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
    2.27 +equivalence.  Thus the automatic tools will apply it automatically. The second
    2.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
    2.29  introduction rule, this is dangerous: the recursion slows down and may
    2.30  even kill the automatic tactics.
    2.31