author nipkow Wed, 18 Oct 2000 17:19:24 +0200 changeset 10243 f11d37d4472d parent 10242 028f54cd2cc9 child 10244 61824cf550db
*** empty log message ***
--- a/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 18 17:19:18 2000 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy	Wed Oct 18 17:19:24 2000 +0200
@@ -3,6 +3,7 @@
section{*The reflexive transitive closure*}

text{*\label{sec:rtc}
+
{\bf Say something about inductive relations as opposed to sets? Or has that
been said already? If not, explain induction!}

@@ -24,9 +25,9 @@
The function @{term rtc} is annotated with concrete syntax: instead of
@{text"rtc r"} we can read and write {term"r*"}. The actual definition
consists of two rules. Reflexivity is obvious and is immediately declared an
-equivalence rule.  Thus the automatic tools will apply it automatically. The
-second rule, @{thm[source]rtc_step}, says that we can always add one more
-@{term r}-step to the left. Although we could make @{thm[source]rtc_step} an
+equivalence.  Thus the automatic tools will apply it automatically. The second
+rule, @{thm[source]rtc_step}, says that we can always add one more @{term
+r}-step to the left. Although we could make @{thm[source]rtc_step} an
introduction rule, this is dangerous: the recursion slows down and may
even kill the automatic tactics.

--- a/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:18 2000 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Wed Oct 18 17:19:24 2000 +0200
@@ -6,6 +6,7 @@
%
\begin{isamarkuptext}%
\label{sec:rtc}
+
{\bf Say something about inductive relations as opposed to sets? Or has that
been said already? If not, explain induction!}

@@ -13,7 +14,7 @@
closure of a relation. This concept was already introduced in
\S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
-fixed point because at that point in the theory hierarchy
+fixpoint because at that point in the theory hierarchy
inductive definitions are not yet available. But now they are:%
\end{isamarkuptext}%