diff -r 000000000000 -r a5a9c433f639 src/Tools/expandshort
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/expandshort	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,31 @@
+#! /bin/sh
+#
+#expandshort - shell script to expand shorthand goal commands
+#  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
+#     rewrite_goals_tac on 1-element lists
+#
+# Usage:
+#    expandshort FILE1 ... FILEn
+#
+#  leaves previous versions as XXX~~
+#
+for f in $*
+do
+echo Expanding shorthands in $f. \ Backup file is $f~~
+mv $f $f~~; sed -e '
+s/^ba \([0-9]*\); *$/by (assume_tac \1);/
+s/^br \(.*\) \([0-9]*\); *$/by (rtac \1 \2);/
+s/^brs \(.*\) \([0-9]*\); *$/by (resolve_tac \1 \2);/
+s/^bd \(.*\) \([0-9]*\); *$/by (dtac \1 \2);/
+s/^bds \(.*\) \([0-9]*\); *$/by (dresolve_tac \1 \2);/
+s/^be \(.*\) \([0-9]*\); *$/by (etac \1 \2);/
+s/^bes \(.*\) \([0-9]*\); *$/by (eresolve_tac \1 \2);/
+s/^bw \(.*\); *$/by (rewtac \1);/
+s/^bws \(.*\); *$/by (rewrite_goals_tac \1);/
+s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
+s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
+s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
+s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
+' $f~~ > $f
+done
+echo Finished.