--- a/doc-src/TutorialI/Inductive/Star.thy Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Star.thy Fri Feb 16 06:46:20 2001 +0100
@@ -8,7 +8,7 @@
Relations too can be defined inductively, since they are just sets of pairs.
A perfect example is the function that maps a relation to its
reflexive transitive closure. This concept was already
-introduced in \S\ref{sec:Relations}, where the operator @{text"^*"} was
+introduced in \S\ref{sec:Relations}, where the operator @{text"\<^sup>*"} was
defined as a least fixed point because inductive definitions were not yet
available. But now they are:
*}
@@ -97,7 +97,7 @@
\end{quote}
A similar heuristic for other kinds of inductions is formulated in
\S\ref{sec:ind-var-in-prems}. The @{text rule_format} directive turns
-@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}. Thus in the end we obtain the original
+@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}: in the end we obtain the original
statement of our lemma.
*}
@@ -148,8 +148,7 @@
contains only two rules, and the single step rule is simpler than
transitivity. As a consequence, @{thm[source]rtc.induct} is simpler than
@{thm[source]rtc2.induct}. Since inductive proofs are hard enough
-anyway, we should
-certainly pick the simplest induction schema available.
+anyway, we should always pick the simplest induction schema available.
Hence @{term rtc} is the definition of choice.
\begin{exercise}\label{ex:converse-rtc-step}