diff -r 7007bc8ddae4 -r 3a5d33e8a019 doc-src/TutorialI/Fun/document/fun0.tex --- 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