diff -r f8da11ca4c6e -r 881222d48777 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Tue Mar 13 18:35:48 2001 +0100
@@ -268,6 +268,8 @@
 
 \input{Misc/document/prime_def.tex}
 
+\input{Misc/document/Translations.tex}
+
 
 \section{The Definitional Approach}
 \label{sec:definitional}
@@ -288,6 +290,8 @@
 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}.
+This strict adherence to the definitional approach reduces the risk of 
+soundness errors inside Isabelle/HOL.
 
 \chapter{More Functional Programming}