doc-src/Logics/LK.tex
changeset 3148 f081757ce757
parent 3137 786faf45f1f3
child 5151 1e944fe5ce96
--- a/doc-src/Logics/LK.tex	Fri May 09 10:18:58 1997 +0200
+++ b/doc-src/Logics/LK.tex	Fri May 09 19:41:17 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 {\tt Sequents/LK} in the sources for complete listings of the
-rules and derived rules.
+See theory {\tt Sequents/LK} in the sources for complete listings of
+the rules and derived rules.
 
 
 \begin{figure}