summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |