# HG changeset patch
# User paulson
# Date 1194017917 -3600
# Node ID 3a5d33e8a01994ef8cb0a7747492773ca6f42ff8
# Parent  7007bc8ddae44ab6a22c8391c3f5ded7daec359c
tweaked

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