1.1 --- a/doc-src/TutorialI/fp.tex	Wed Aug 30 18:05:20 2000 +0200
     1.2 +++ b/doc-src/TutorialI/fp.tex	Wed Aug 30 18:09:20 2000 +0200
     1.3 @@ -405,16 +405,12 @@
     1.4  
     1.5  Simplification is one of the central theorem proving tools in Isabelle and
     1.6  many other systems. The tool itself is called the \bfindex{simplifier}. The
     1.7 -purpose of this section is twofold: to introduce the many features of the
     1.8 -simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the
     1.9 -simplifier works (\S\ref{sec:SimpHow}).  Anybody intending to use HOL should
    1.10 -read \S\ref{sec:SimpFeatures}, and the serious student should read
    1.11 -\S\ref{sec:SimpHow} as well in order to understand what happened in case
    1.12 -things do not simplify as expected.
    1.13 -
    1.14 -
    1.15 -\subsection{Using the simplifier}
    1.16 -\label{sec:SimpFeatures}
    1.17 +purpose of this section is introduce the many features of the simplifier.
    1.18 +Anybody intending to use HOL should read this section. Later on
    1.19 +(\S\ref{sec:simplification-II}) we explain some more advanced features and a
    1.20 +little bit of how the simplifier works. The serious student should read that
    1.21 +section as well, in particular in order to understand what happened if things
    1.22 +do not simplify as expected.
    1.23  
    1.24  \subsubsection{What is simplification}
    1.25  
    1.26 @@ -572,11 +568,11 @@
    1.27  inductive proofs. The first one we have already mentioned in our initial
    1.28  example:
    1.29  \begin{quote}
    1.30 -{\em 1. Theorems about recursive functions are proved by induction.}
    1.31 +\emph{Theorems about recursive functions are proved by induction.}
    1.32  \end{quote}
    1.33  In case the function has more than one argument
    1.34  \begin{quote}
    1.35 -{\em 2. Do induction on argument number $i$ if the function is defined by
    1.36 +\emph{Do induction on argument number $i$ if the function is defined by
    1.37  recursion in argument number $i$.}
    1.38  \end{quote}
    1.39  When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @
    1.40 @@ -598,8 +594,8 @@
    1.41  side, the simpler \isa{rev} on the right-hand side. This constitutes
    1.42  another, albeit weak heuristic that is not restricted to induction:
    1.43  \begin{quote}
    1.44 -  {\em 5. The right-hand side of an equation should (in some sense) be
    1.45 -    simpler than the left-hand side.}
    1.46 +  \emph{The right-hand side of an equation should (in some sense) be simpler
    1.47 +    than the left-hand side.}
    1.48  \end{quote}
    1.49  The heuristic is tricky to apply because it is not obvious that
    1.50  \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what