--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Oct 11 09:09:06 2000 +0200
@@ -251,14 +251,18 @@
\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
\begin{isamarkuptext}%
Finally we should mention that HOL already provides the mother of all
-inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
+inductions, \textbf{wellfounded
+induction}\indexbold{induction!wellfounded}\index{wellfounded
+induction|see{induction, wellfounded}} (\isa{wf{\isacharunderscore}induct}):
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
\end{isabelle}
-where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
+where \isa{wf\ r} means that the relation \isa{r} is wellfounded
+(see \S\ref{sec:wellfounded}).
For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and
derived) as a special case of \isa{wf{\isacharunderscore}induct} where
-\isa{r} is \isa{{\isacharless}} on \isa{nat}. For details see the library.%
+\isa{r} is \isa{{\isacharless}} on \isa{nat}. The details can be found in the HOL library.
+For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables: