--- a/doc-src/TutorialI/Advanced/advanced.tex Wed Oct 11 12:52:56 2000 +0200
+++ b/doc-src/TutorialI/Advanced/advanced.tex Wed Oct 11 13:15:04 2000 +0200
@@ -18,6 +18,16 @@
covers two topics: how to define recursive function over nested recursive datatypes
and how to establish termination by means other than measure functions.
+If, after reading this section, you feel that the definition of recursive
+functions is overly and maybe unnecessarily complicated by the requirement of
+totality, you should ponder the alternative, a logic of partial functions,
+where recursive definitions are always wellformed. For a start, 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 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{Recursion over nested datatypes}
\label{sec:nested-recdef}
\input{Recdef/document/Nested0.tex}