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