--- a/src/Tools/expandshort Mon Oct 07 10:41:26 1996 +0200
+++ b/src/Tools/expandshort Mon Oct 07 10:43:40 1996 +0200
@@ -14,16 +14,16 @@
do
echo Expanding shorthands in $f. \ Backup file is $f~~
mv $f $f~~; sed -e '
-s/^by(/by (/
-s/^ba \([0-9]*\);/by (assume_tac \1);/
-s/^br \([^;]*\) \([0-9]*\);/by (rtac \1 \2);/
-s/^brs \([^;]*\) \([0-9]*\);/by (resolve_tac \1 \2);/
-s/^bd \([^;]*\) \([0-9]*\);/by (dtac \1 \2);/
-s/^bds \([^;]*\) \([0-9]*\);/by (dresolve_tac \1 \2);/
-s/^be \([^;]*\) \([0-9]*\);/by (etac \1 \2);/
-s/^bes \([^;]*\) \([0-9]*\);/by (eresolve_tac \1 \2);/
-s/^bw \([^;]*\);/by (rewtac \1);/
-s/^bws \([^;]*\);/by (rewrite_goals_tac \1);/
+s/\<by(/by (/
+s/\<ba \([0-9][0-9]*\);/by (assume_tac \1);/
+s/\<br \([^;]*\) \([0-9][0-9]*\);/by (rtac \1 \2);/
+s/\<brs \([^;]*\) \([0-9][0-9]*\);/by (resolve_tac \1 \2);/
+s/\<bd \([^;]*\) \([0-9][0-9]*\);/by (dtac \1 \2);/
+s/\<bds \([^;]*\) \([0-9][0-9]*\);/by (dresolve_tac \1 \2);/
+s/\<be \([^;]*\) \([0-9][0-9]*\);/by (etac \1 \2);/
+s/\<bes \([^;]*\) \([0-9][0-9]*\);/by (eresolve_tac \1 \2);/
+s/\<bw \([^;]*\);/by (rewtac \1);/
+s/\<bws \([^;]*\);/by (rewrite_goals_tac \1);/
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g