fixed ref to srcs;
authorwenzelm
Wed, 07 May 1997 18:36:13 +0200
changeset 3137 786faf45f1f3
parent 3136 7d940ceb25b5
child 3138 6c0c7e99312d
fixed ref to srcs;
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}