1.1 --- a/expandshort	Mon Nov 08 17:52:24 1993 +0100
     1.2 +++ b/expandshort	Tue Nov 09 11:02:01 1993 +0100
     1.3 @@ -13,15 +13,15 @@
     1.4  do
     1.5  echo Expanding shorthands in $f. \ Backup file is $f~~
     1.6  mv $f $f~~; sed -e '
     1.7 -s/^ba \([0-9]*\); *$/by (assume_tac \1);/
     1.8 -s/^br \(.*\) \([0-9]*\); *$/by (rtac \1 \2);/
     1.9 -s/^brs \(.*\) \([0-9]*\); *$/by (resolve_tac \1 \2);/
    1.10 -s/^bd \(.*\) \([0-9]*\); *$/by (dtac \1 \2);/
    1.11 -s/^bds \(.*\) \([0-9]*\); *$/by (dresolve_tac \1 \2);/
    1.12 -s/^be \(.*\) \([0-9]*\); *$/by (etac \1 \2);/
    1.13 -s/^bes \(.*\) \([0-9]*\); *$/by (eresolve_tac \1 \2);/
    1.14 -s/^bw \(.*\); *$/by (rewtac \1);/
    1.15 -s/^bws \(.*\); *$/by (rewrite_goals_tac \1);/
    1.16 +s/^ba \([0-9]*\);/by (assume_tac \1);/
    1.17 +s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/
    1.18 +s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/
    1.19 +s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/
    1.20 +s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/
    1.21 +s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/
    1.22 +s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/
    1.23 +s/^bw \([^;]*\);/by (rewtac \1);/
    1.24 +s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
    1.25  s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
    1.26  s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
    1.27  s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g

     2.1 --- a/src/Tools/expandshort	Mon Nov 08 17:52:24 1993 +0100
     2.2 +++ b/src/Tools/expandshort	Tue Nov 09 11:02:01 1993 +0100
     2.3 @@ -13,15 +13,15 @@
     2.4  do
     2.5  echo Expanding shorthands in $f. \ Backup file is $f~~
     2.6  mv $f $f~~; sed -e '
     2.7 -s/^ba \([0-9]*\); *$/by (assume_tac \1);/
     2.8 -s/^br \(.*\) \([0-9]*\); *$/by (rtac \1 \2);/
     2.9 -s/^brs \(.*\) \([0-9]*\); *$/by (resolve_tac \1 \2);/
    2.10 -s/^bd \(.*\) \([0-9]*\); *$/by (dtac \1 \2);/
    2.11 -s/^bds \(.*\) \([0-9]*\); *$/by (dresolve_tac \1 \2);/
    2.12 -s/^be \(.*\) \([0-9]*\); *$/by (etac \1 \2);/
    2.13 -s/^bes \(.*\) \([0-9]*\); *$/by (eresolve_tac \1 \2);/
    2.14 -s/^bw \(.*\); *$/by (rewtac \1);/
    2.15 -s/^bws \(.*\); *$/by (rewrite_goals_tac \1);/
    2.16 +s/^ba \([0-9]*\);/by (assume_tac \1);/
    2.17 +s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/
    2.18 +s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/
    2.19 +s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/
    2.20 +s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/
    2.21 +s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/
    2.22 +s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/
    2.23 +s/^bw \([^;]*\);/by (rewtac \1);/
    2.24 +s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
    2.25  s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
    2.26  s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
    2.27  s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g