equal
deleted
inserted
replaced
78 RLN : thm list * (int * thm list) -> thm list \hfill{\bf infix} |
78 RLN : thm list * (int * thm list) -> thm list \hfill{\bf infix} |
79 RL : thm list * thm list -> thm list \hfill{\bf infix} |
79 RL : thm list * thm list -> thm list \hfill{\bf infix} |
80 MRL : thm list list * thm list -> thm list \hfill{\bf infix} |
80 MRL : thm list list * thm list -> thm list \hfill{\bf infix} |
81 \end{ttbox} |
81 \end{ttbox} |
82 Joining rules together is a simple way of deriving new rules. These |
82 Joining rules together is a simple way of deriving new rules. These |
83 functions are especially useful with destruction rules. |
83 functions are especially useful with destruction rules. To store |
|
84 the result in the theorem database, use \ttindex{bind_thm} |
|
85 (\S\ref{ExtractingAndStoringTheProvedTheorem}). |
84 \begin{ttdescription} |
86 \begin{ttdescription} |
85 \item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN} |
87 \item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN} |
86 resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$. |
88 resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$. |
87 Unless there is precisely one resolvent it raises exception |
89 Unless there is precisely one resolvent it raises exception |
88 \xdx{THM}; in that case, use {\tt RLN}. |
90 \xdx{THM}; in that case, use {\tt RLN}. |