doc-src/TutorialI/Misc/AdvancedInd.thy

 
 theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
 by(insert induct_lem, blast);
 
 text{*
+
 Finally we should mention that HOL already provides the mother of all
-inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
-@{thm[display]"wf_induct"[no_vars]}
-where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
+inductions, \textbf{wellfounded
+induction}\indexbold{induction!wellfounded}\index{wellfounded
+induction|see{induction, wellfounded}} (@{thm[source]wf_induct}):
+@{thm[display]wf_induct[no_vars]}
+where @{term"wf r"} means that the relation @{term r} is wellfounded
+(see \S\ref{sec:wellfounded}).
 For example, theorem @{thm[source]nat_less_induct} can be viewed (and
 derived) as a special case of @{thm[source]wf_induct} where 
-@{term"r"} is @{text"<"} on @{typ"nat"}. For details see the library.
+@{term r} is @{text"<"} on @{typ nat}. The details can be found in the HOL library.
+For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}.
 *};
 
 (*<*)
 end
 (*>*)