# HG changeset patch
# User paulson
# Date 1141121233 -3600
# Node ID d81fae81f385ac67aa22391dca2d08949207d2fd
# Parent  66e841b1001eb82d20c124d37ea58ac4f5072559
typos

diff -r 66e841b1001e -r d81fae81f385 doc-src/Logics/LK.tex
--- 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