diff -r f43fa07536c0 -r eddc69b55fac doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Fri Mar 09 19:05:48 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Mon Mar 12 18:17:45 2001 +0100
@@ -269,6 +269,26 @@
 \input{Misc/document/prime_def.tex}
 
 
+\section{The Definitional Approach}
+\label{sec:definitional}
+
+As we pointed out at the beginning of the chapter, asserting arbitrary
+axioms, e.g. $f(n) = f(n) + 1$, may easily lead to contradictions. In order
+to avoid this danger, this tutorial advocates the definitional rather than
+the axiomatic approach: introduce new concepts by definitions, thus
+preserving consistency. However, on the face of it, Isabelle/HOL seems to
+support many more constructs than just definitions, for example
+\isacommand{primrec}. The crucial point is that internally, everything
+(except real axioms) is reduced to a definition. For example, given some
+\isacommand{primrec} function definition, this is turned into a proper
+(nonrecursive!) definition, and the user-supplied recursion equations are
+derived as theorems from the definition. This tricky process is completely
+hidden from the user and it is not necessary to understand the details. The
+result of the definitional approach is that \isacommand{primrec} is as safe
+as pure \isacommand{defs} are, but more convenient. And this is not just the
+case for \isacommand{primrec} but also for the other commands described
+later, like \isacommand{recdef} and \isacommand{inductive}.
+
 \chapter{More Functional Programming}
 
 The purpose of this chapter is to deepen the reader's understanding of the