--- a/doc-src/TutorialI/fp.tex Mon Mar 19 10:37:47 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Mon Mar 19 12:38:36 2001 +0100
@@ -284,7 +284,7 @@
(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
+derived as theorems from that 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