diff -r 5652018b809a -r 07b13770c4d6 doc-src/TutorialI/fp.tex
--- 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}