diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -405,16 +405,12 @@
 
 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 twofold: to introduce the many features of the
-simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the
-simplifier works (\S\ref{sec:SimpHow}).  Anybody intending to use HOL should
-read \S\ref{sec:SimpFeatures}, and the serious student should read
-\S\ref{sec:SimpHow} as well in order to understand what happened in case
-things do not simplify as expected.
-
-
-\subsection{Using the simplifier}
-\label{sec:SimpFeatures}
+purpose of this section is introduce the many features of the simplifier.
+Anybody intending to use 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.
 
 \subsubsection{What is simplification}
 
@@ -572,11 +568,11 @@
 inductive proofs. The first one we have already mentioned in our initial
 example:
 \begin{quote}
-{\em 1. Theorems about recursive functions are proved by induction.}
+\emph{Theorems about recursive functions are proved by induction.}
 \end{quote}
 In case the function has more than one argument
 \begin{quote}
-{\em 2. Do induction on argument number $i$ if the function is defined by
+\emph{Do induction on argument number $i$ if the function is defined by
 recursion in argument number $i$.}
 \end{quote}
 When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @
@@ -598,8 +594,8 @@
 side, the simpler \isa{rev} on the right-hand side. This constitutes
 another, albeit weak heuristic that is not restricted to induction:
 \begin{quote}
-  {\em 5. The right-hand side of an equation should (in some sense) be
-    simpler than the left-hand side.}
+  \emph{The right-hand side of an equation should (in some sense) be simpler
+    than the left-hand side.}
 \end{quote}
 The heuristic is tricky to apply because it is not obvious that
 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what