doc-src/TutorialI/Misc/AdvancedInd.thy

--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Thu Nov 01 20:20:19 2007 +0100
@@ -155,7 +155,7 @@
 txt{*\noindent
 To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use
 the same general induction method as for recursion induction (see
-\S\ref{sec:recdef-induction}):
+\S\ref{sec:fun-induction}):
 *};
 
 apply(induct_tac k rule: nat_less_induct);