diff -r 7ef380745743 -r 5ab08609e6c8 doc-src/TutorialI/Inductive/Star.thy
--- 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)