doc-src/Logics/LK.tex
changeset 3137 786faf45f1f3
parent 841 14b96e3bd4ab
child 3148 f081757ce757
equal deleted inserted replaced
3136:7d940ceb25b5 3137:786faf45f1f3
   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 the files {\tt LK/LK.thy} and {\tt LK/LK.ML}
   225 See {\tt Sequents/LK} in the sources for complete listings of the
   226 for complete listings of the rules and derived rules.
   226 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