# HG changeset patch
# User paulson
# Date 886159919 -3600
# Node ID f88e466c43fa08aaf42cabfa970e283b84a045d0
# Parent  9f8f931e0089a04c7dcd52c087a2067275d279b0
Fixed the description of recdef

diff -r 9f8f931e0089 -r f88e466c43fa doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Jan 30 11:34:06 1998 +0100
+++ b/doc-src/Logics/HOL.tex	Fri Jan 30 12:31:59 1998 +0100
@@ -1985,6 +1985,11 @@
     "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
 \end{ttbox}
 
+With \texttt{recdef}, function definitions may be incomplete, and patterns may
+overlap, as in functional programming.  The \texttt{recdef} package
+disambiguates overlapping patterns by taking the order of rules into account.
+For missing patterns, the function is defined to return an arbitrary value.
+
 The well-founded relation defines a notion of ``smaller'' for the function's
 argument type.  The relation $\prec$ is \textbf{well-founded} provided it
 admits no infinitely decreasing chains
@@ -2028,7 +2033,7 @@
     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
 \end{ttbox}
 
-The general form of a primitive recursive definition is
+The general form of a well-founded recursive definition is
 \begin{ttbox}
 recdef {\it function} {\it rel}
     congs   {\it congruence rules}      {\bf(optional)}
@@ -2057,9 +2062,8 @@
   left-hand side must have the form $f\,t$, where $f$ is the function and $t$
   is a tuple of distinct variables.  If more than one equation is present then
   $f$ is defined by pattern-matching on components of its argument whose type
-  is a \texttt{datatype}.  The patterns must be exhaustive and
-  non-overlapping.  
-  
+  is a \texttt{datatype}.  
+
   Unlike with \texttt{primrec}, the reduction rules are not added to the
   default simpset, and individual rules may not be labelled with identifiers.
   However, the identifier $f$\texttt{.rules} is visible at the \ML\ level