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
     1 #! /bin/sh
     2 #
     3 #expandshort - shell script to expand shorthand goal commands
     4 #  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
     5 #     rewrite_goals_tac on 1-element lists
     6 #
     7 # Usage:
     8 #    expandshort FILE1 ... FILEn
     9 #
    10 #  leaves previous versions as XXX~~
    11 #
    12 for f in $*
    13 do
    14 echo Expanding shorthands in $f. \ Backup file is $f~~
    15 mv $f $f~~; sed -e '
    16 s/^ba \([0-9]*\);/by (assume_tac \1);/
    17 s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/
    18 s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/
    19 s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/
    20 s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/
    21 s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/
    22 s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/
    23 s/^bw \([^;]*\);/by (rewtac \1);/
    24 s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
    25 s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
    26 s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \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
    29 ' $f~~ > $f
    30 done
    31 echo Finished.