diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/fp.tex	Thu Nov 01 20:20:19 2007 +0100
@@ -194,7 +194,7 @@
 becomes smaller with every recursive call. There must be at most one equation
 for each constructor.  Their order is immaterial.
 A more general method for defining total recursive functions is introduced in
-{\S}\ref{sec:recdef}.
+{\S}\ref{sec:fun}.
 
 \begin{exercise}\label{ex:Tree}
 \input{Misc/document/Tree.tex}%
@@ -265,7 +265,7 @@
 (nonrecursive!) definition from which the user-supplied recursion equations are
 automatically proved.  This process is
 hidden from the user, who does not have to understand the details.  Other commands described
-later, like \isacommand{recdef} and \isacommand{inductive}, work similarly.  
+later, like \isacommand{fun} and \isacommand{inductive}, work similarly.  
 This strict adherence to the definitional approach reduces the risk of 
 soundness errors.
 
@@ -281,9 +281,9 @@
 study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
 datatypes, including those involving function spaces, are covered in
 {\S}\ref{sec:advanced-datatypes}; it closes with another case study, search
-trees (``tries'').  Finally we introduce \isacommand{recdef}, a general
+trees (``tries'').  Finally we introduce \isacommand{fun}, a general
 form of recursive function definition that goes well beyond 
-\isacommand{primrec} ({\S}\ref{sec:recdef}).
+\isacommand{primrec} ({\S}\ref{sec:fun}).
 
 
 \section{Simplification}
@@ -460,35 +460,18 @@
 \index{tries|)}
 
 \section{Total Recursive Functions}
-\label{sec:recdef}
-\index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(}
+\label{sec:fun}
+\index{fun@\isacommand {fun} (command)|(}\index{functions!total|(}
 
 Although many total functions have a natural primitive recursive definition,
 this is not always the case. Arbitrary total recursive functions can be
-defined by means of \isacommand{recdef}: you can use full pattern-matching,
+defined by means of \isacommand{fun}: you can use full pattern-matching,
 recursion need not involve datatypes, and termination is proved by showing
-that the arguments of all recursive calls are smaller in a suitable (user
-supplied) sense. In this section we restrict ourselves to measure functions;
-more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
-
-\subsection{Defining Recursive Functions}
-\label{sec:recdef-examples}
-\input{Recdef/document/examples.tex}
-
-\subsection{Proving Termination}
-\input{Recdef/document/termination.tex}
+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}.
 
-\subsection{Simplification and Recursive Functions}
-\label{sec:recdef-simplification}
-\input{Recdef/document/simplification.tex}
+\input{Fun/document/fun0.tex}
 
-\subsection{Induction and Recursive Functions}
-\index{induction!recursion|(}
-\index{recursion induction|(}
-
-\input{Recdef/document/Induction.tex}
-\label{sec:recdef-induction}
-
-\index{induction!recursion|)}
-\index{recursion induction|)}
-\index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)}
+\index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}