diff -r c7686ac6c240 -r 8d309beb66d6 doc-src/TutorialI/Advanced/advanced.tex
--- 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)|)}