--- a/doc-src/TutorialI/Fun/document/fun0.tex Fri Nov 02 16:38:14 2007 +0100
+++ b/doc-src/TutorialI/Fun/document/fun0.tex Fri Nov 02 16:38:37 2007 +0100
@@ -123,7 +123,7 @@
\subsection{Simplification}
\label{sec:fun-simplification}
-Upon successful termination proof, the recursion equations become
+Upon a successful termination proof, the recursion equations become
simplification rules, just as with \isacommand{primrec}.
In most cases this works fine, but there is a subtle
problem that must be mentioned: simplification may not
--- a/doc-src/TutorialI/Fun/fun0.thy Fri Nov 02 16:38:14 2007 +0100
+++ b/doc-src/TutorialI/Fun/fun0.thy Fri Nov 02 16:38:37 2007 +0100
@@ -105,7 +105,7 @@
\subsection{Simplification}
\label{sec:fun-simplification}
-Upon successful termination proof, the recursion equations become
+Upon a successful termination proof, the recursion equations become
simplification rules, just as with \isacommand{primrec}.
In most cases this works fine, but there is a subtle
problem that must be mentioned: simplification may not