author | paulson |
Thu, 26 Sep 1996 17:30:52 +0200 | |
changeset 2041 | a3262b93c1d2 |
parent 2040 | 6db93e6f1b11 |
child 2042 | 33b4c1624e26 |
--- a/src/Tools/expandshort Thu Sep 26 17:15:19 1996 +0200 +++ b/src/Tools/expandshort Thu Sep 26 17:30:52 1996 +0200 @@ -28,6 +28,7 @@ s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g +s/rtac *(\([a-zA-Z0-9_]*\) *RS *ssubst) */stac \1 /g ' $f~~ | expand > $f done echo Finished.