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