lib/scripts/expandshort.pl
changeset 4478 9c5a0eef74ff
parent 4417 44ff59be6031
child 4592 ff0c5c57fdfb
     1.1 --- a/lib/scripts/expandshort.pl	Wed Dec 24 10:02:30 1997 +0100
     1.2 +++ b/lib/scripts/expandshort.pl	Wed Dec 24 10:42:27 1997 +0100
     1.3 @@ -3,6 +3,8 @@
     1.4  #
     1.5  # expandshort.pl - expand shorthand goal commands
     1.6  #
     1.7 +# in "be ... i;" -> "by (etac ... i);" the "..." phrase is not allowed to
     1.8 +#   contain punctuation.  Otherwise, comments can be affected!
     1.9  
    1.10  sub expandshort {
    1.11      my ($file) = @_;
    1.12 @@ -18,15 +20,15 @@
    1.13      s/ *\(Safe_tac\)/ Safe_tac/sg;
    1.14      s/\bby\(/by (/sg;
    1.15      s/\bba\b *(\d+);/by (assume_tac \1);/sg;
    1.16 -    s/\bbr\b *([^;]*) (\d+);/by (rtac \1 \2);/sg;
    1.17 -    s/\bbrs\b *([^;]*) (\d+);/by (resolve_tac \1 \2);/sg;
    1.18 -    s/\bbd\b *([^;]*) (\d+);/by (dtac \1 \2);/sg;
    1.19 -    s/\bbds\b *([^;]*) (\d+);/by (dresolve_tac \1 \2);/sg;
    1.20 -    s/\bbe\b *([^;]*) (\d+);/by (etac \1 \2);/sg;
    1.21 -    s/\bbes\b *([^;]*) (\d+);/by (eresolve_tac \1 \2);/sg;
    1.22 -    s/\bbw\b *([^;]*);/by (rewtac \1);/sg;
    1.23 -    s/\bbws\b *([^;]*);/by (rewrite_goals_tac \1);/sg;
    1.24 -    s/\bauto *\(\)/by (Auto_tac())/sg;
    1.25 +    s/\bbr\b *([^;.*!]*) (\d+);/by (rtac \1 \2);/sg;
    1.26 +    s/\bbrs\b *([^;.*!]*) (\d+);/by (resolve_tac \1 \2);/sg;
    1.27 +    s/\bbd\b *([^;.*!]*) (\d+);/by (dtac \1 \2);/sg;
    1.28 +    s/\bbds\b *([^;.*!]*) (\d+);/by (dresolve_tac \1 \2);/sg;
    1.29 +    s/\bbe\b *([^;.*!]*) (\d+);/by (etac \1 \2);/sg;
    1.30 +    s/\bbes\b *([^;.*!]*) (\d+);/by (eresolve_tac \1 \2);/sg;
    1.31 +    s/\bbw\b *([^;.*!]*);/by (rewtac \1);/sg;
    1.32 +    s/\bbws\b *([^;.*!]*);/by (rewrite_goals_tac \1);/sg;
    1.33 +    s/\bauto *\(\)/by Auto_tac/sg;
    1.34      s/dresolve_tac *\[(\w+)\] */dtac \1 /sg;
    1.35      s/eresolve_tac *\[(\w+)\] */etac \1 /sg;
    1.36      s/resolve_tac *\[(\w+)\] */rtac \1 /sg;