equal
deleted
inserted
replaced
31 s/\bbw\b *([^;*!]*);/by (rewtac $1);/sg; |
31 s/\bbw\b *([^;*!]*);/by (rewtac $1);/sg; |
32 s/\bbws\b *([^;*!]*);/by (rewrite_goals_tac $1);/sg; |
32 s/\bbws\b *([^;*!]*);/by (rewrite_goals_tac $1);/sg; |
33 s/\bauto *\(\)/by Auto_tac/sg; |
33 s/\bauto *\(\)/by Auto_tac/sg; |
34 s/dresolve_tac *\[(\w+)\] */dtac $1 /sg; |
34 s/dresolve_tac *\[(\w+)\] */dtac $1 /sg; |
35 s/eresolve_tac *\[(\w+)\] */etac $1 /sg; |
35 s/eresolve_tac *\[(\w+)\] */etac $1 /sg; |
|
36 s/forward_tac *\[(\w+)\] */ftac $1 /sg; |
36 s/resolve_tac *\[(\w+)\] */rtac $1 /sg; |
37 s/resolve_tac *\[(\w+)\] */rtac $1 /sg; |
37 s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac $1$2/sg; |
38 s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac $1$2/sg; |
38 s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac $1 /sg; |
39 s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac $1 /sg; |
39 |
40 |
40 $result = $_; |
41 $result = $_; |