# HG changeset patch
# User paulson
# Date 826550286 -3600
# Node ID 02bbdc811ae7764378c5e2319fa22212311df0f3
# Parent  a203d206fab75236737a52b863afaae7725485cd
Now catches "by(" too

diff -r a203d206fab7 -r 02bbdc811ae7 src/Tools/expandshort
--- a/src/Tools/expandshort	Mon Mar 11 14:16:35 1996 +0100
+++ b/src/Tools/expandshort	Mon Mar 11 14:18:06 1996 +0100
@@ -14,6 +14,7 @@
 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);/