diff -r a18f3bce7198 -r 1e5585fd3632 doc-src/System/misc.tex --- a/doc-src/System/misc.tex Mon Sep 06 18:19:12 1999 +0200 +++ b/doc-src/System/misc.tex Mon Sep 06 22:12:08 1999 +0200 @@ -33,10 +33,10 @@ \begin{ttbox} Usage: expandshort [FILES|DIRS...] - Recursively find .ML files, expand shorthand goal commands. - Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac, - rewrite_goals_tac on 1-element lists; furthermore expands tabs, - since they are now forbidden in ML string constants. + Recursively find .ML files, expand shorthand goal commands. Also + contracts uses of resolve_tac, dresolve_tac, eresolve_tac, + forward_tac, rewrite_goals_tac on 1-element lists; furthermore expands + tabs, which are forbidden in SML string constants. Renames old versions of files by appending "~~". \end{ttbox}