# HG changeset patch
# User paulson
# Date 861786730 -7200
# Node ID 7ffe67afeb94847d25bd7431965949c515c534f9
# Parent  39806db47be93e22626420e33caa60db12d4c89b
Unfortunately, the \\< syntax does not always accept the beginning of a line

diff -r 39806db47be9 -r 7ffe67afeb94 src/Tools/expandshort
--- a/src/Tools/expandshort	Wed Apr 23 11:11:38 1997 +0200
+++ b/src/Tools/expandshort	Wed Apr 23 11:12:10 1997 +0200
@@ -15,17 +15,17 @@
 echo Expanding shorthands in $f. \ Backup file is $f~~
 if [ ! -s $f ]; then echo "File $f is EMPTY!!"; exit 1; fi
 mv $f $f~~; sed -e '
-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/\<auto *()/by (Auto_tac())/
+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/^auto *()/by (Auto_tac())/
 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