expandshort
changeset 96 91e8875e9c45
parent 0 a5a9c433f639
equal deleted inserted replaced
95:2246a80b1cb5 96:91e8875e9c45
    11 #
    11 #
    12 for f in $*
    12 for f in $*
    13 do
    13 do
    14 echo Expanding shorthands in $f. \ Backup file is $f~~
    14 echo Expanding shorthands in $f. \ Backup file is $f~~
    15 mv $f $f~~; sed -e '
    15 mv $f $f~~; sed -e '
    16 s/^ba \([0-9]*\); *$/by (assume_tac \1);/
    16 s/^ba \([0-9]*\);/by (assume_tac \1);/
    17 s/^br \(.*\) \([0-9]*\); *$/by (rtac \1 \2);/
    17 s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/
    18 s/^brs \(.*\) \([0-9]*\); *$/by (resolve_tac \1 \2);/
    18 s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/
    19 s/^bd \(.*\) \([0-9]*\); *$/by (dtac \1 \2);/
    19 s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/
    20 s/^bds \(.*\) \([0-9]*\); *$/by (dresolve_tac \1 \2);/
    20 s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/
    21 s/^be \(.*\) \([0-9]*\); *$/by (etac \1 \2);/
    21 s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/
    22 s/^bes \(.*\) \([0-9]*\); *$/by (eresolve_tac \1 \2);/
    22 s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/
    23 s/^bw \(.*\); *$/by (rewtac \1);/
    23 s/^bw \([^;]*\);/by (rewtac \1);/
    24 s/^bws \(.*\); *$/by (rewrite_goals_tac \1);/
    24 s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
    25 s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
    25 s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
    26 s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
    26 s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
    27 s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
    27 s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
    28 s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
    28 s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
    29 ' $f~~ > $f
    29 ' $f~~ > $f