# 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}