--- a/src/Tools/expandshort Tue Dec 16 12:17:48 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-#! /usr/bin/perl -pi~~
-# $Id$
-#Shell script to expand shorthand goal commands
-# ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
-# rewrite_goals_tac on 1-element lists
-# [Tabs are forbidden in strings. Use "expand" or "untabify" in emacs".]
-#
-# Usage:
-# expandshort FILE1 ... FILEn
-#
-#Renames old versions of the files as FILE1~~ ... FILEn~~
-#
-s/\bsafe_tac *\(claset *\( *\) *\)/Safe_tac/;
-s/ *\(Safe_tac\) *([0-9]+)/ Safe_tac \1/;
-s/ *\(Safe_tac\)/ Safe_tac/;
-s/\bby\(/by (/;
-s/\bba\b *(\d+);/by (assume_tac \1);/;
-s/\bbr\b *([^;]*) (\d+);/by (rtac \1 \2);/;
-s/\bbrs\b *([^;]*) (\d+);/by (resolve_tac \1 \2);/;
-s/\bbd\b *([^;]*) (\d+);/by (dtac \1 \2);/;
-s/\bbds\b *([^;]*) (\d+);/by (dresolve_tac \1 \2);/;
-s/\bbe\b *([^;]*) (\d+);/by (etac \1 \2);/;
-s/\bbes\b *([^;]*) (\d+);/by (eresolve_tac \1 \2);/;
-s/\bbw\b *([^;]*);/by (rewtac \1);/;
-s/\bbws\b *([^;]*);/by (rewrite_goals_tac \1);/;
-s/\bauto *\(\)/by (Auto_tac())/;
-s/dresolve_tac *\[(\w+)\] */dtac \1 /g;
-s/eresolve_tac *\[(\w+)\] */etac \1 /g;
-s/resolve_tac *\[(\w+)\] */rtac \1 /g;
-s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac \1\2/g;
-s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac \1 /g;