Unfortunately, the \\< syntax does not always accept the beginning of a line
authorpaulson
Wed, 23 Apr 1997 11:12:10 +0200
changeset 3022 7ffe67afeb94
parent 3021 39806db47be9
child 3023 01364e2f30ad
Unfortunately, the \\< syntax does not always accept the beginning of a line
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