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 |