1.1 --- a/doc-src/TutorialI/fp.tex	Mon Mar 12 18:23:11 2001 +0100
     1.2 +++ b/doc-src/TutorialI/fp.tex	Tue Mar 13 18:35:48 2001 +0100
     1.3 @@ -268,6 +268,8 @@
     1.4  
     1.5  \input{Misc/document/prime_def.tex}
     1.6  
     1.7 +\input{Misc/document/Translations.tex}
     1.8 +
     1.9  
    1.10  \section{The Definitional Approach}
    1.11  \label{sec:definitional}
    1.12 @@ -288,6 +290,8 @@
    1.13  as pure \isacommand{defs} are, but more convenient. And this is not just the
    1.14  case for \isacommand{primrec} but also for the other commands described
    1.15  later, like \isacommand{recdef} and \isacommand{inductive}.
    1.16 +This strict adherence to the definitional approach reduces the risk of 
    1.17 +soundness errors inside Isabelle/HOL.
    1.18  
    1.19  \chapter{More Functional Programming}
    1.20