doc-src/Ref/simplifier.tex
changeset 7990 0a604b2fc2b1
parent 7920 1ee85d4205b2
child 8136 8c65f3ca13f2
     1.1 --- a/doc-src/Ref/simplifier.tex	Sun Oct 31 15:26:37 1999 +0100
     1.2 +++ b/doc-src/Ref/simplifier.tex	Sun Oct 31 20:11:23 1999 +0100
     1.3 @@ -502,7 +502,8 @@
     1.4  
     1.5  \subsection{*The subgoaler}\label{sec:simp-subgoaler}
     1.6  \begin{ttbox}
     1.7 -setsubgoaler : simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
     1.8 +setsubgoaler :
     1.9 +  simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
    1.10  prems_of_ss  : simpset -> thm list
    1.11  \end{ttbox}
    1.12  
    1.13 @@ -794,7 +795,7 @@
    1.14  \end{warn}
    1.15  
    1.16  
    1.17 -\section{Examples of using the simplifier}
    1.18 +\section{Examples of using the Simplifier}
    1.19  \index{examples!of simplification} Assume we are working within {\tt
    1.20    FOL} (see the file \texttt{FOL/ex/Nat}) and that
    1.21  \begin{ttdescription}
    1.22 @@ -1239,7 +1240,7 @@
    1.23  prove particular theorems depending on the current redex.
    1.24  
    1.25  
    1.26 -\section{*Setting up the simplifier}\label{sec:setting-up-simp}
    1.27 +\section{*Setting up the Simplifier}\label{sec:setting-up-simp}
    1.28  \index{simplification!setting up}
    1.29  
    1.30  Setting up the simplifier for new logics is complicated.  This section