1.1 --- a/lib/scripts/expandshort.pl	Mon Aug 17 11:00:57 1998 +0200
     1.2 +++ b/lib/scripts/expandshort.pl	Mon Aug 17 13:06:29 1998 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  #
     1.5  # in "be ... i;" -> "by (etac ... i);" the "..." phrase is not allowed to
     1.6  #   contain punctuation.  Otherwise, comments can be affected!
     1.7 +# a special case is made to detect    be alpha.alpha digits   
     1.8  
     1.9  sub expandshort {
    1.10      my ($file) = @_;
    1.11 @@ -20,14 +21,15 @@
    1.12      s/ *\(Safe_tac\)/ Safe_tac/sg;
    1.13      s/\bby\(/by (/sg;
    1.14      s/\bba\b *(\d+);/by (assume_tac $1);/sg;
    1.15 -    s/\bbr\b *([^;.*!]*) (\d+);/by (rtac $1 $2);/sg;
    1.16 -    s/\bbrs\b *([^;.*!]*) (\d+);/by (resolve_tac $1 $2);/sg;
    1.17 -    s/\bbd\b *([^;.*!]*) (\d+);/by (dtac $1 $2);/sg;
    1.18 -    s/\bbds\b *([^;.*!]*) (\d+);/by (dresolve_tac $1 $2);/sg;
    1.19 +    s/\bbr\b *([^;*!]*) (\d+);/by (rtac $1 $2);/sg;
    1.20 +    s/\bbrs\b *([^;*!]*) (\d+);/by (resolve_tac $1 $2);/sg;
    1.21 +    s/\bbd\b *([^;*!]*) (\d+);/by (dtac $1 $2);/sg;
    1.22 +    s/\bbds\b *([^;*!]*) (\d+);/by (dresolve_tac $1 $2);/sg;
    1.23      s/\bbe\b *([^;.*!]*) (\d+);/by (etac $1 $2);/sg;
    1.24 -    s/\bbes\b *([^;.*!]*) (\d+);/by (eresolve_tac $1 $2);/sg;
    1.25 -    s/\bbw\b *([^;.*!]*);/by (rewtac $1);/sg;
    1.26 -    s/\bbws\b *([^;.*!]*);/by (rewrite_goals_tac $1);/sg;
    1.27 +    s/\bbe\b *(\w+\.\w+) (\d+);/by (etac $1 $2);/sg;
    1.28 +    s/\bbes\b *([^;*!]*) (\d+);/by (eresolve_tac $1 $2);/sg;
    1.29 +    s/\bbw\b *([^;*!]*);/by (rewtac $1);/sg;
    1.30 +    s/\bbws\b *([^;*!]*);/by (rewrite_goals_tac $1);/sg;
    1.31      s/\bauto *\(\)/by Auto_tac/sg;
    1.32      s/dresolve_tac *\[(\w+)\] */dtac $1 /sg;
    1.33      s/eresolve_tac *\[(\w+)\] */etac $1 /sg;