
diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- 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%




