doc-src/Ref/simplifier.tex

 most users should never worry about them.
 
 \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
 rewrite rules, while \ttindex{delsimps} deletes rewrite rules from a
 simpset.