Declares the function exit_use to behave like use but fail if
errors are detected. It can be used in all Makefiles except Pure, which will
write the exception handler explicitly ("exit" will have been declared
already).
#! /bin/sh
# simp FILE1 ... FILEn
#
# leaves previous versions as XXX~~
#
for f in $*
do
echo $f. \ Backup file is $f~~
mv $f $f~~; sed -e '
s/\<ASM_SIMP_TAC\>/asm_simp_tac/g
s/\<SIMP_TAC\>/simp_tac/g
s/\<addrews\>/addsimps/g
s/addsplits \(\[[^]]*\]\)/setloop (split_tac \1)/g
s/addsplits/setloop split_tac/g
s/\<setauto\>/setsolver/g
' $f~~ > $f
done
echo Finished.