--- a/doc-src/TutorialI/Advanced/advanced.tex Wed Oct 11 09:09:06 2000 +0200
+++ b/doc-src/TutorialI/Advanced/advanced.tex Wed Oct 11 10:44:42 2000 +0200
@@ -14,6 +14,10 @@
\section{Advanced forms of recursion}
\index{*recdef|(}
+The purpose of this section is to introduce advanced forms of \isacommand{recdef}. It
+covers two topics: how to define recursive function over nested recursive datatypes
+and how to establish termination by means other than measure functions.
+
\subsection{Recursion over nested datatypes}
\label{sec:nested-recdef}
\input{Recdef/document/Nested0.tex}
@@ -23,7 +27,7 @@
\subsection{Beyond measure}
\label{sec:wellfounded}
-\input{Recdef/document/WFrec.tex}
+\input{Advanced/document/WFrec.tex}
\section{Advanced induction techniques}
\label{sec:advanced-ind}