--- a/doc-src/TutorialI/fp.tex Tue Feb 20 10:18:26 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Tue Feb 20 10:37:12 2001 +0100
@@ -297,7 +297,7 @@
Simplification is one of the central theorem proving tools in Isabelle and
many other systems. The tool itself is called the \bfindex{simplifier}. The
-purpose of this section is introduce the many features of the simplifier.
+purpose of this section is to introduce the many features of the simplifier.
Anybody intending to perform proofs in HOL should read this section. Later on
({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
little bit of how the simplifier works. The serious student should read that
@@ -466,7 +466,7 @@
defined by means of \isacommand{recdef}: you can use full pattern-matching,
recursion need not involve datatypes, and termination is proved by showing
that the arguments of all recursive calls are smaller in a suitable (user
-supplied) sense. In this section we ristrict ourselves to measure functions;
+supplied) sense. In this section we restrict ourselves to measure functions;
more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
\subsection{Defining Recursive Functions}