--- 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}
--- a/lib/Tools/expandshort Mon Sep 06 18:19:12 1999 +0200
+++ b/lib/Tools/expandshort Mon Sep 06 22:12:08 1999 +0200
@@ -12,10 +12,10 @@
echo
echo "Usage: $PRG [FILES|DIRS...]"
echo
- echo " Recursively find .ML files, expand shorthand goal commands."
- echo " Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac,"
- echo " rewrite_goals_tac on 1-element lists; furthermore expands tabs,"
- echo " since they are now forbidden in ML string constants."
+ echo " Recursively find .ML files, expand shorthand goal commands. Also"
+ echo " contracts uses of resolve_tac, dresolve_tac, eresolve_tac,"
+ echo " forward_tac, rewrite_goals_tac on 1-element lists; furthermore expands"
+ echo " tabs, which are forbidden in SML string constants."
echo
echo " Renames old versions of files by appending \"~~\"."
echo