lots of internal cleaning and tuning;
removed {parse,print}_{pre,post}_proc;
new lexer: now human readable due to scanner combinators;
new parser installed, but still inactive (due to grammar ambiguities);
added Syntax.test_read;
typ_of_term: sorts now made distinct and sorted;
mixfix: added forced line breaks (//);
PROP now printed before subterm of type prop with non-const head;
#! /bin/sh
#
#expandshort - shell script to expand shorthand goal commands
# ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
# rewrite_goals_tac on 1-element lists
#
# Usage:
# expandshort FILE1 ... FILEn
#
# leaves previous versions as XXX~~
#
for f in $*
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/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
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
' $f~~ > $f
done
echo Finished.