1.1 --- a/doc-src/TutorialI/fp.tex	Thu Nov 01 13:44:44 2007 +0100
     1.2 +++ b/doc-src/TutorialI/fp.tex	Thu Nov 01 20:20:19 2007 +0100
     1.3 @@ -194,7 +194,7 @@
     1.4  becomes smaller with every recursive call. There must be at most one equation
     1.5  for each constructor.  Their order is immaterial.
     1.6  A more general method for defining total recursive functions is introduced in
     1.7 -{\S}\ref{sec:recdef}.
     1.8 +{\S}\ref{sec:fun}.
     1.9  
    1.10  \begin{exercise}\label{ex:Tree}
    1.11  \input{Misc/document/Tree.tex}%
    1.12 @@ -265,7 +265,7 @@
    1.13  (nonrecursive!) definition from which the user-supplied recursion equations are
    1.14  automatically proved.  This process is
    1.15  hidden from the user, who does not have to understand the details.  Other commands described
    1.16 -later, like \isacommand{recdef} and \isacommand{inductive}, work similarly.  
    1.17 +later, like \isacommand{fun} and \isacommand{inductive}, work similarly.  
    1.18  This strict adherence to the definitional approach reduces the risk of 
    1.19  soundness errors.
    1.20  
    1.21 @@ -281,9 +281,9 @@
    1.22  study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
    1.23  datatypes, including those involving function spaces, are covered in
    1.24  {\S}\ref{sec:advanced-datatypes}; it closes with another case study, search
    1.25 -trees (``tries'').  Finally we introduce \isacommand{recdef}, a general
    1.26 +trees (``tries'').  Finally we introduce \isacommand{fun}, a general
    1.27  form of recursive function definition that goes well beyond 
    1.28 -\isacommand{primrec} ({\S}\ref{sec:recdef}).
    1.29 +\isacommand{primrec} ({\S}\ref{sec:fun}).
    1.30  
    1.31  
    1.32  \section{Simplification}
    1.33 @@ -460,35 +460,18 @@
    1.34  \index{tries|)}
    1.35  
    1.36  \section{Total Recursive Functions}
    1.37 -\label{sec:recdef}
    1.38 -\index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(}
    1.39 +\label{sec:fun}
    1.40 +\index{fun@\isacommand {fun} (command)|(}\index{functions!total|(}
    1.41  
    1.42  Although many total functions have a natural primitive recursive definition,
    1.43  this is not always the case. Arbitrary total recursive functions can be
    1.44 -defined by means of \isacommand{recdef}: you can use full pattern-matching,
    1.45 +defined by means of \isacommand{fun}: you can use full pattern-matching,
    1.46  recursion need not involve datatypes, and termination is proved by showing
    1.47 -that the arguments of all recursive calls are smaller in a suitable (user
    1.48 -supplied) sense. In this section we restrict ourselves to measure functions;
    1.49 -more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
    1.50 +that the arguments of all recursive calls are smaller in a suitable sense.
    1.51 +In this section we restrict ourselves to functions where Isabelle can prove
    1.52 +termination automatically. User supplied termination proofs are discussed in
    1.53 +{\S}\ref{sec:beyond-measure}.
    1.54  
    1.55 -\subsection{Defining Recursive Functions}
    1.56 -\label{sec:recdef-examples}
    1.57 -\input{Recdef/document/examples.tex}
    1.58 +\input{Fun/document/fun0.tex}
    1.59  
    1.60 -\subsection{Proving Termination}
    1.61 -\input{Recdef/document/termination.tex}
    1.62 -
    1.63 -\subsection{Simplification and Recursive Functions}
    1.64 -\label{sec:recdef-simplification}
    1.65 -\input{Recdef/document/simplification.tex}
    1.66 -
    1.67 -\subsection{Induction and Recursive Functions}
    1.68 -\index{induction!recursion|(}
    1.69 -\index{recursion induction|(}
    1.70 -
    1.71 -\input{Recdef/document/Induction.tex}
    1.72 -\label{sec:recdef-induction}
    1.73 -
    1.74 -\index{induction!recursion|)}
    1.75 -\index{recursion induction|)}
    1.76 -\index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)}
    1.77 +\index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}