doc-src/TutorialI/fp.tex

 need to understand the ingredients of \isa{auto}.  This section covers the
 method that \isa{auto} always applies first, simplification.
 
 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
 section as well, in particular in order to understand what happened if things
 do not simplify as expected.

 Although many total functions have a natural primitive recursive definition,
 this is not always the case. Arbitrary total recursive functions can be
 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}
 \label{sec:recdef-examples}
 \input{Recdef/document/examples.tex}