doc-src/Ref/simplifier.tex

 to prove the goal.  
 
 
 \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}
 
 The subgoaler is the tactic used to solve subgoals arising out of
 conditional rewrite rules or congruence rules.  The default should be

   in ordinary proof scripts.  The main intention is to provide an
   internal interface to the simplifier for special utilities.
 \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}
 \item[Nat.thy] 
   is a theory including the constants $0$, $Suc$ and $+$,

 grained control over rule application, beyond higher-order pattern
 matching.  Usually, procedures would do some more work, in particular
 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
 describes how the simplifier is installed for intuitionistic
 first-order logic; the code is largely taken from {\tt