doc-src/Ref/simplifier.tex
 changeset 122 db9043a8e372 parent 104 d8205bb279a7 child 133 2322fd6d57a1
equal inserted replaced
121:d392174734e9 122:db9043a8e372
    25 most users should never worry about them.
    25 most users should never worry about them.
    26
    26
    27 \subsection{Rewrite rules}\index{rewrite rules}
    27 \subsection{Rewrite rules}\index{rewrite rules}
    28
    28
    29 Rewrite rules are theorems like $Suc(\Var{m}) + \Var{n} = \Var{m} +  29 Rewrite rules are theorems like$Suc(\Var{m}) + \Var{n} = \Var{m} +
    30 Suc(\Var{n})$,$\Var{P}\conj\Var{P} \bimp \Var{P}$, or$\Var{A} \un \Var{B}
    30 Suc(\Var{n})$,$\Var{P}\conj\Var{P} \bimp \Var{P}$, or$\Var{A} \union \Var{B}
    31 \equiv \{x.x\in A \disj x\in B\}$. {\bf Conditional} rewrites such as  31 \equiv \{x.x\in A \disj x\in B\}$.  {\bf Conditional} rewrites such as
    32 $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 0$ are permitted; the conditions
    32 $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 0$ are permitted; the conditions
    33 can be arbitrary terms.  The infix operation \ttindex{addsimps} adds new
    33 can be arbitrary terms.  The infix operation \ttindex{addsimps} adds new
    34 rewrite rules, while \ttindex{delsimps} deletes rewrite rules from a
    34 rewrite rules, while \ttindex{delsimps} deletes rewrite rules from a
    35 simpset.
    35 simpset.