author paulson Fri, 02 Nov 2007 16:38:37 +0100 changeset 25265 3a5d33e8a019 parent 25264 7007bc8ddae4 child 25266 37aa898e0523
tweaked
--- 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