removed advanced recdef section and replaced it by citation of Alex's tutorial.

--- a/doc-src/TutorialI/Advanced/ROOT.ML	Mon Nov 05 15:04:19 2007 +0100
+++ b/doc-src/TutorialI/Advanced/ROOT.ML	Mon Nov 05 15:37:41 2007 +0100
@@ -1,5 +1,2 @@
 use "../settings.ML";
-no_document use_thy "While_Combinator";
 use_thy "simp";
-use_thy "WFrec";
-use_thy "Partial";

--- a/doc-src/TutorialI/Advanced/advanced.tex	Mon Nov 05 15:04:19 2007 +0100
+++ b/doc-src/TutorialI/Advanced/advanced.tex	Mon Nov 05 15:37:41 2007 +0100
@@ -1,51 +1,49 @@
-\chapter{Advanced Simplification, Recursion and Induction}
+\chapter{Advanced Simplification and Induction}
 
-Although we have already learned a lot about simplification, recursion and
+Although we have already learned a lot about simplification and
 induction, there are some advanced proof techniques that we have not covered
-yet and which are worth learning. The three sections of this chapter are almost
-independent of each other and can be read in any order. Only the notion of
-\emph{congruence rules}, introduced in the section on simplification, is
-required for parts of the section on recursion.
+yet and which are worth learning. The sections of this chapter are
+independent of each other and can be read in any order.
 
 \input{Advanced/document/simp.tex}
 
-\section{Advanced Forms of Recursion}
-\index{recdef@\isacommand {recdef} (command)|(}
-
-This section introduces advanced forms of
-\isacommand{recdef}: how to establish termination by means other than measure
-functions, how to define recursive functions over nested recursive datatypes
-and how to deal with partial functions.
-
-If, after reading this section, you feel that the definition of recursive
-functions is overly complicated by the requirement of
-totality, you should ponder the alternatives.  In a logic of partial functions,
-recursive definitions are always accepted.  But there are many
-such logics, and no clear winner has emerged. And in all of these logics you
-are (more or less frequently) required to reason about the definedness of
-terms explicitly. Thus one shifts definedness arguments from definition time to
-proof time. In HOL you may have to work hard to define a function, but proofs
-can then proceed unencumbered by worries about undefinedness.
-
-\subsection{Beyond Measure}
-\label{sec:beyond-measure}
-\input{Advanced/document/WFrec.tex}
-
-\subsection{Recursion Over Nested Datatypes}
-\label{sec:nested-recdef}
-\input{Recdef/document/Nested0.tex}
-\input{Recdef/document/Nested1.tex}
-\input{Recdef/document/Nested2.tex}
-
-\subsection{Partial Functions}
-\index{functions!partial}
-\input{Advanced/document/Partial.tex}
-
-\index{recdef@\isacommand {recdef} (command)|)}
-
 \section{Advanced Induction Techniques}
 \label{sec:advanced-ind}
 \index{induction|(}
 \input{Misc/document/AdvancedInd.tex}
 \input{CTL/document/CTLind.tex}
 \index{induction|)}
+
+%\section{Advanced Forms of Recursion}
+%\index{recdef@\isacommand {recdef} (command)|(}
+
+%This section introduces advanced forms of
+%\isacommand{recdef}: how to establish termination by means other than measure
+%functions, how to define recursive functions over nested recursive datatypes
+%and how to deal with partial functions.
+%
+%If, after reading this section, you feel that the definition of recursive
+%functions is overly complicated by the requirement of
+%totality, you should ponder the alternatives.  In a logic of partial functions,
+%recursive definitions are always accepted.  But there are many
+%such logics, and no clear winner has emerged. And in all of these logics you
+%are (more or less frequently) required to reason about the definedness of
+%terms explicitly. Thus one shifts definedness arguments from definition time to
+%proof time. In HOL you may have to work hard to define a function, but proofs
+%can then proceed unencumbered by worries about undefinedness.
+
+%\subsection{Beyond Measure}
+%\label{sec:beyond-measure}
+%\input{Advanced/document/WFrec.tex}
+%
+%\subsection{Recursion Over Nested Datatypes}
+%\label{sec:nested-recdef}
+%\input{Recdef/document/Nested0.tex}
+%\input{Recdef/document/Nested1.tex}
+%\input{Recdef/document/Nested2.tex}
+%
+%\subsection{Partial Functions}
+%\index{functions!partial}
+%\input{Advanced/document/Partial.tex}
+%
+%\index{recdef@\isacommand {recdef} (command)|)}

--- a/doc-src/TutorialI/Datatype/Nested.thy	Mon Nov 05 15:04:19 2007 +0100
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Mon Nov 05 15:37:41 2007 +0100
@@ -142,17 +142,17 @@
 
 declare subst_App [simp del]
 
-text{*\noindent
-The advantage is that now we have replaced @{const substs} by
-@{term map}, we can profit from the large number of pre-proved lemmas
-about @{term map}.  Unfortunately inductive proofs about type
-@{text term} are still awkward because they expect a conjunction. One
-could derive a new induction principle as well (see
-\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
-and to define functions with \isacommand{fun} instead.
-Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below,
-and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can 
-handle nested recursion.
+text{*\noindent The advantage is that now we have replaced @{const
+substs} by @{const map}, we can profit from the large number of
+pre-proved lemmas about @{const map}.  Unfortunately, inductive proofs
+about type @{text term} are still awkward because they expect a
+conjunction. One could derive a new induction principle as well (see
+\S\ref{sec:derive-ind}), but simpler is to stop using
+\isacommand{primrec} and to define functions with \isacommand{fun}
+instead.  Simple uses of \isacommand{fun} are described in
+\S\ref{sec:fun} below.  Advanced applications, including functions
+over nested datatypes like @{text term}, are discussed in a
+separate tutorial~\cite{isabelle-function}.
 
 Of course, you may also combine mutual and nested recursion of datatypes. For example,
 constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of

--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Nov 05 15:04:19 2007 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Nov 05 15:37:41 2007 +0100
@@ -206,17 +206,16 @@
 \isacommand{declare}\isamarkupfalse%
 \ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}%
 \begin{isamarkuptext}%
-\noindent
-The advantage is that now we have replaced \isa{substs} by
-\isa{map}, we can profit from the large number of pre-proved lemmas
-about \isa{map}.  Unfortunately inductive proofs about type
-\isa{term} are still awkward because they expect a conjunction. One
-could derive a new induction principle as well (see
-\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
-and to define functions with \isacommand{fun} instead.
-Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below,
-and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can 
-handle nested recursion.
+\noindent The advantage is that now we have replaced \isa{substs} by \isa{map}, we can profit from the large number of
+pre-proved lemmas about \isa{map}.  Unfortunately, inductive proofs
+about type \isa{term} are still awkward because they expect a
+conjunction. One could derive a new induction principle as well (see
+\S\ref{sec:derive-ind}), but simpler is to stop using
+\isacommand{primrec} and to define functions with \isacommand{fun}
+instead.  Simple uses of \isacommand{fun} are described in
+\S\ref{sec:fun} below.  Advanced applications, including functions
+over nested datatypes like \isa{term}, are discussed in a
+separate tutorial~\cite{isabelle-function}.
 
 Of course, you may also combine mutual and nested recursion of datatypes. For example,
 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of

--- a/doc-src/TutorialI/IsaMakefile	Mon Nov 05 15:04:19 2007 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Mon Nov 05 15:37:41 2007 +0100
@@ -4,7 +4,7 @@
 
 ## targets
 
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Recdef \
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \
   HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Complex-Types HOL-Misc \
   HOL-Protocol HOL-Documents styles
 images:
@@ -104,23 +104,11 @@
 	@rm -f tutorial.dvi
 
 
-## HOL-Recdef
-
-HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
-
-$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \
-  Recdef/simplification.thy Recdef/Induction.thy \
-  Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy
-	$(USEDIR) Recdef
-	@rm -f tutorial.dvi
-
-
 ## HOL-Advanced
 
 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
 
-$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \
-	Advanced/Partial.thy
+$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
 	$(USEDIR) Advanced
 	@rm -f tutorial.dvi
 
@@ -205,4 +193,4 @@
 ## clean
 
 clean:
-	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex
+	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Fun.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex

--- a/doc-src/TutorialI/Sets/sets.tex	Mon Nov 05 15:04:19 2007 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Mon Nov 05 15:37:41 2007 +0100
@@ -876,8 +876,8 @@
 \index{relations!well-founded|(}%
 A well-founded relation captures the notion of a terminating
 process. Complex recursive functions definitions must specify a
-well-founded relation that justifies their termination
-({\S}\ref{sec:beyond-measure}).  Most of the forms of induction found
+well-founded relation that justifies their
+termination~\cite{isabelle-function}. Most of the forms of induction found
 in mathematics are merely special cases of induction over a
 well-founded relation.
 

--- a/doc-src/TutorialI/fp.tex	Mon Nov 05 15:04:19 2007 +0100
+++ b/doc-src/TutorialI/fp.tex	Mon Nov 05 15:37:41 2007 +0100
@@ -469,8 +469,9 @@
 recursion need not involve datatypes, and termination is proved by showing
 that the arguments of all recursive calls are smaller in a suitable sense.
 In this section we restrict ourselves to functions where Isabelle can prove
-termination automatically. User supplied termination proofs are discussed in
-{\S}\ref{sec:beyond-measure}.
+termination automatically. More advanced function definitions, including user
+supplied termination proofs, nested recursion and partiality, are discussed
+in a separate tutorial~\cite{isabelle-function}.
 
 \input{Fun/document/fun0.tex}