diff -r 2246a80b1cb5 -r 91e8875e9c45 expandshort
--- a/expandshort	Mon Nov 08 17:52:24 1993 +0100
+++ b/expandshort	Tue Nov 09 11:02:01 1993 +0100
@@ -13,15 +13,15 @@
 do
 echo Expanding shorthands in $f. \ Backup file is $f~~
 mv $f $f~~; sed -e '
-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/^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/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