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%