diff -r d1415164b814 -r 751fde5307e4 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Fri Aug 25 12:17:09 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Mon Aug 28 09:32:51 2000 +0200
@@ -534,7 +534,8 @@
 where the list of \emph{modifiers} helps to fine tune the behaviour and may
 be empty. Most if not all of the proofs seen so far could have been performed
 with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
-only the first subgoal and may thus need to be repeated.
+only the first subgoal and may thus need to be repeated---use \isaindex{simp_all}
+to simplify all subgoals.
 Note that \isa{simp} fails if nothing changes.
 
 \subsubsection{Adding and deleting simplification rules}
@@ -851,10 +852,12 @@
 \index{induction!recursion|)}
 \index{recursion induction|)}
 
-%\subsection{Advanced forms of recursion}
+\subsection{Advanced forms of recursion}
+\label{sec:advanced-recdef}
 
-%\input{Recdef/document/Nested0.tex}
-%\input{Recdef/document/Nested1.tex}
+\input{Recdef/document/Nested0.tex}
+\input{Recdef/document/Nested1.tex}
+\input{Recdef/document/Nested2.tex}
 
 \index{*recdef|)}