# 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/\