expandshort
author lcp
Mon Dec 13 18:50:03 1993 +0100 (1993-12-13)
changeset 196 7646f5b4653c
parent 96 91e8875e9c45
permissions -rwxr-xr-x
added isabelle-users paragraph
clasohm@0
     1
#! /bin/sh
clasohm@0
     2
#
clasohm@0
     3
#expandshort - shell script to expand shorthand goal commands
clasohm@0
     4
#  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
clasohm@0
     5
#     rewrite_goals_tac on 1-element lists
clasohm@0
     6
#
clasohm@0
     7
# Usage:
clasohm@0
     8
#    expandshort FILE1 ... FILEn
clasohm@0
     9
#
clasohm@0
    10
#  leaves previous versions as XXX~~
clasohm@0
    11
#
clasohm@0
    12
for f in $*
clasohm@0
    13
do
clasohm@0
    14
echo Expanding shorthands in $f. \ Backup file is $f~~
clasohm@0
    15
mv $f $f~~; sed -e '
lcp@96
    16
s/^ba \([0-9]*\);/by (assume_tac \1);/
lcp@96
    17
s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/
lcp@96
    18
s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/
lcp@96
    19
s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/
lcp@96
    20
s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/
lcp@96
    21
s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/
lcp@96
    22
s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/
lcp@96
    23
s/^bw \([^;]*\);/by (rewtac \1);/
lcp@96
    24
s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
clasohm@0
    25
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
clasohm@0
    26
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
clasohm@0
    27
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
clasohm@0
    28
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
clasohm@0
    29
' $f~~ > $f
clasohm@0
    30
done
clasohm@0
    31
echo Finished.