doc-src/Logics/LK.tex

--- a/doc-src/Logics/LK.tex	Wed May 07 18:35:56 1997 +0200
+++ b/doc-src/Logics/LK.tex	Wed May 07 18:36:13 1997 +0200
@@ -222,8 +222,8 @@
 {\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}
-for complete listings of the rules and derived rules.
+See {\tt Sequents/LK} in the sources for complete listings of the
+rules and derived rules.
 
 
 \begin{figure}