--- 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}