# HG changeset patch
# User paulson
# Date 844677820 -7200
# Node ID 8d4558d95e9a58f27916df37abac14cff2dcade5
# Parent  b14a08bf61bf164ae679eb330108a48f08c94ad9
Now replaces shorthand commands even if indented

diff -r b14a08bf61bf -r 8d4558d95e9a src/Tools/expandshort
--- 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