doc-src/TutorialI/Sets/sets.tex
 changeset 10374 d72638f2b78e parent 10373 f9211fc8cd7d child 10398 cdb451206ef9
--- a/doc-src/TutorialI/Sets/sets.tex	Fri Nov 03 17:14:06 2000 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Fri Nov 03 17:57:00 2000 +0100
@@ -883,13 +883,15 @@
Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
infinite  descending chains
$\cdots \prec a@2 \prec a@1 \prec a@0.$
-If $\prec$ is well-founded then it can be used with the well-founded
-induction rule:
+If $\prec$ is well-founded then it can be used with the \textbf{well-founded
+induction}\indexbold{induction!well-founded}\index{well-founded
+induction|see{induction, well-founded}} rule:
$\infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}}$
To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for
arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$.
Intuitively, the well-foundedness of $\prec$ ensures that the chains of
-reasoning are finite.
+reasoning are finite.  For a fuller account of well-founded relations and
\begin{isabelle}