New unified treatment of sequent calculi by Sara Kalvala
combines the old LK and Modal with the new ILL (Int. Linear Logic)
#! /bin/sh
# $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
# ALSO expands tabs, since they are now forbidden in strings.
#
# Usage:
# expandshort FILE1 ... FILEn
#
#Renames old versions of the files as FILE1~~ ... FILEn~~
#
for f in $*
do
echo Expanding shorthands in $f. \ Backup file is $f~~
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/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.