# HG changeset patch
# User nipkow
# Date 895670428 -7200
# Node ID 15fd948d6c69c6392082e784a53ac5b122fa30fd
# Parent  d8e5c6e31854db7fd49d465ead0e780ae4d802d8
Small mods.

diff -r d8e5c6e31854 -r 15fd948d6c69 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Tue May 19 17:16:18 1998 +0200
+++ b/doc-src/Ref/simplifier.tex	Wed May 20 15:20:28 1998 +0200
@@ -360,7 +360,7 @@
 \index{rewrite rules|)}
 
 
-\subsection{Simplification procedures}
+\subsection{*Simplification procedures}
 \begin{ttbox}
 addsimprocs : simpset * simproc list -> simpset
 delsimprocs : simpset * simproc list -> simpset
@@ -926,9 +926,6 @@
 
 \section{Permutative rewrite rules}
 \index{rewrite rules!permutative|(}
-\begin{ttbox}
-settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}
-\end{ttbox}
 
 A rewrite rule is {\bf permutative} if the left-hand side and right-hand
 side are the same up to renaming of variables.  The most common permutative
@@ -942,6 +939,9 @@
 lexicographic ordering on terms.  This should be perfectly OK in most
 cases, but can be changed for special applications.
 
+\begin{ttbox}
+settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}
+\end{ttbox}
 \begin{ttdescription}
   
 \item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as