equal
deleted
inserted
replaced
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. |