src/Tools/expandshort

Now a Perl script. No longer requires commands to be at the beginnings of
lines. RESTRICTION: no longer expands tabs to spaces. No longer lists the
files it is altering.

+
−#! /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/\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;