# HG changeset patch
# User wenzelm
# Date 863022973 -7200
# Node ID 786faf45f1f3a359d1f1bd04e8c1901e08748a33
# Parent  7d940ceb25b5144f849bd8730da5c217ed9ba1c9
fixed ref to srcs;

diff -r 7d940ceb25b5 -r 786faf45f1f3 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}