author | wenzelm |
Wed, 07 May 1997 18:36:13 +0200 | |
changeset 3137 | 786faf45f1f3 |
parent 3136 | 7d940ceb25b5 |
child 3138 | 6c0c7e99312d |
--- 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}