summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 28 Feb 2006 11:07:13 +0100 | |

changeset 19152 | d81fae81f385 |

parent 19151 | 66e841b1001e |

child 19153 | 0864119a9611 |

typos

--- a/doc-src/Logics/LK.tex Mon Feb 27 17:37:37 2006 +0100 +++ b/doc-src/Logics/LK.tex Tue Feb 28 11:07:13 2006 +0100 @@ -27,7 +27,7 @@ isabelle Sequents context LK.thy; \end{ttbox} -Model logic and linear logic are also available, but unfortunately they are +Modal logic and linear logic are also available, but unfortunately they are not documented. @@ -305,7 +305,7 @@ According to the cut-elimination theorem, the cut rule can be eliminated from proofs of sequents. But the rule is still essential. It can be used to structure a proof into lemmas, avoiding repeated proofs of the same -formula. More importantly, the cut rule can not be eliminated from +formula. More importantly, the cut rule cannot be eliminated from derivations of rules. For example, there is a trivial cut-free proof of the sequent \(P\conj Q\turn Q\conj P\). Noting this, we might want to derive a rule for swapping the conjuncts