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}