equal
deleted
inserted
replaced
220 but are incomplete. Multiple use of a quantifier can be obtained by a |
220 but are incomplete. Multiple use of a quantifier can be obtained by a |
221 contraction rule, which in backward proof duplicates a formula. The tactic |
221 contraction rule, which in backward proof duplicates a formula. The tactic |
222 {\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules, |
222 {\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules, |
223 specifying the formula to duplicate. |
223 specifying the formula to duplicate. |
224 |
224 |
225 See {\tt Sequents/LK} in the sources for complete listings of the |
225 See theory {\tt Sequents/LK} in the sources for complete listings of |
226 rules and derived rules. |
226 the rules and derived rules. |
227 |
227 |
228 |
228 |
229 \begin{figure} |
229 \begin{figure} |
230 \begin{ttbox} |
230 \begin{ttbox} |
231 \tdx{conR} $H |- $E, P, $F, P ==> $H |- $E, P, $F |
231 \tdx{conR} $H |- $E, P, $F, P ==> $H |- $E, P, $F |