--- a/doc-src/Ref/simplifier.tex Tue Nov 16 14:10:19 1993 +0100
+++ b/doc-src/Ref/simplifier.tex Tue Nov 16 14:13:11 1993 +0100
@@ -27,7 +27,7 @@
\subsection{Rewrite rules}\index{rewrite rules}
Rewrite rules are theorems like $Suc(\Var{m}) + \Var{n} = \Var{m} +
-Suc(\Var{n})$, $\Var{P}\conj\Var{P} \bimp \Var{P}$, or $\Var{A} \un \Var{B}
+Suc(\Var{n})$, $\Var{P}\conj\Var{P} \bimp \Var{P}$, or $\Var{A} \union \Var{B}
\equiv \{x.x\in A \disj x\in B\}$. {\bf Conditional} rewrites such as
$\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 0$ are permitted; the conditions
can be arbitrary terms. The infix operation \ttindex{addsimps} adds new