diff -r 01b87a921967 -r 2ca08f62df33 doc-src/Logics/LK.tex
--- a/doc-src/Logics/LK.tex	Fri Apr 22 18:18:37 1994 +0200
+++ b/doc-src/Logics/LK.tex	Fri Apr 22 18:43:49 1994 +0200
@@ -222,7 +222,7 @@
 {\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
 specifying the formula to duplicate.
 
-See the files {\tt LK/lk.thy} and {\tt LK/lk.ML}
+See the files {\tt LK/LK.thy} and {\tt LK/LK.ML}
 for complete listings of the rules and derived rules.
 
 
@@ -296,7 +296,7 @@
 \end{ttbox}
 Associative unification is not as efficient as it might be, in part because
 the representation of lists defeats some of Isabelle's internal
-optimizations.  The following operations implement faster rule application,
+optimisations.  The following operations implement faster rule application,
 and may have other uses.
 \begin{ttdescription}
 \item[\ttindexbold{forms_of_seq} {\it t}]