# HG changeset patch
# User wenzelm
# Date 936648728 -7200
# Node ID 1e5585fd36324bb979fae1cdd569415744722ce5
# Parent  a18f3bce71988df9cf16b7b098cea73bed5f31bf
expandshort usage: forward_tac;

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}
diff -r a18f3bce7198 -r 1e5585fd3632 lib/Tools/expandshort
--- 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