diff -r 50ca726466c6 -r 0a604b2fc2b1 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/simplifier.tex	Sun Oct 31 20:11:23 1999 +0100
@@ -502,7 +502,8 @@
 
 \subsection{*The subgoaler}\label{sec:simp-subgoaler}
 \begin{ttbox}
-setsubgoaler : simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
+setsubgoaler :
+  simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
 prems_of_ss  : simpset -> thm list
 \end{ttbox}
 
@@ -794,7 +795,7 @@
 \end{warn}
 
 
-\section{Examples of using the simplifier}
+\section{Examples of using the Simplifier}
 \index{examples!of simplification} Assume we are working within {\tt
   FOL} (see the file \texttt{FOL/ex/Nat}) and that
 \begin{ttdescription}
@@ -1239,7 +1240,7 @@
 prove particular theorems depending on the current redex.
 
 
-\section{*Setting up the simplifier}\label{sec:setting-up-simp}
+\section{*Setting up the Simplifier}\label{sec:setting-up-simp}
 \index{simplification!setting up}
 
 Setting up the simplifier for new logics is complicated.  This section