--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Nov 01 20:20:19 2007 +0100
@@ -216,7 +216,7 @@
\noindent
To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use
the same general induction method as for recursion induction (see
-\S\ref{sec:recdef-induction}):%
+\S\ref{sec:fun-induction}):%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%