diff -r d10abc8c11fb -r 866957616069 lib/Tools/expandshort
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/expandshort	Thu Jan 23 14:35:15 1997 +0100
@@ -0,0 +1,57 @@
+#!/bin/bash -norc
+#
+# $Id$
+#
+# DESCRIPTION: expand shorthand goal commands
+
+
+PRG=$(basename $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [FILES ...]"
+  echo
+  echo "Expand shorthand goal commands in FILES.  Also contracts uses of"
+  echo "resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on"
+  echo "1-element lists; furthermore expands tabs, since they are now"
+  echo "forbidden in strings."
+  echo
+  echo "Renames old versions of FILES by appending \"~~\"."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## main
+
+for f in "$@"
+do
+echo Expanding shorthands in $f. \ Backup file is $f~~
+if [ ! -s $f ]; then echo "File $f is EMPTY!!"; exit 1; fi
+mv $f $f~~; sed -e '
+s/\<by(/by (/
+s/\<ba \([0-9][0-9]*\);/by (assume_tac \1);/
+s/\<br \([^;]*\) \([0-9][0-9]*\);/by (rtac \1 \2);/
+s/\<brs \([^;]*\) \([0-9][0-9]*\);/by (resolve_tac \1 \2);/
+s/\<bd \([^;]*\) \([0-9][0-9]*\);/by (dtac \1 \2);/
+s/\<bds \([^;]*\) \([0-9][0-9]*\);/by (dresolve_tac \1 \2);/
+s/\<be \([^;]*\) \([0-9][0-9]*\);/by (etac \1 \2);/
+s/\<bes \([^;]*\) \([0-9][0-9]*\);/by (eresolve_tac \1 \2);/
+s/\<bw \([^;]*\);/by (rewtac \1);/
+s/\<bws \([^;]*\);/by (rewrite_goals_tac \1);/
+s/\<auto *()/by (Auto_tac())/
+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
+s/rtac *(\([a-zA-Z0-9_]*\)  *RS  *ssubst)  */stac \1 /g
+' $f~~ | expand > $f
+done
+echo Finished.