--- a/doc-src/TutorialI/Inductive/Star.thy Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Star.thy Mon Nov 06 11:32:23 2000 +0100
@@ -8,10 +8,9 @@
A perfect example of an inductive definition is the reflexive transitive
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 @{text"^*"} is not defined inductively but via a least
-fixed point because at that point in the theory hierarchy
-inductive definitions are not yet available. But now they are:
+\S\ref{sec:Relations}, where the operator @{text"^*"} was
+defined as a least fixed point because
+inductive definitions were not yet available. But now they are:
*}
consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)