Now replaces uses of ssubst by stac
authorpaulson
Thu, 26 Sep 1996 17:30:52 +0200
changeset 2041 a3262b93c1d2
parent 2040 6db93e6f1b11
child 2042 33b4c1624e26
Now replaces uses of ssubst by stac
src/Tools/expandshort
--- 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.