expandshort

well_ord_iso_predE replaces not_well_ord_iso_pred

well_ord_iso_unique: eliminated a premise using well_ord_ord_iso

Proved well_ord_iso_pred_eq, ord_iso_image_pred, ord_iso_restrict_pred,
part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso, well_ord_ord_iso,
well_ord_iso_preserving, mono_map_is_fun, mono_map_is_inj, mono_map_trans,
mono_ord_isoI, well_ord_mono_ord_isoI, ord_iso_is_mono_map,
ord_iso_map_mono_map, ord_iso_map_ord_iso, domain_ord_iso_map_subset,
domain_ord_iso_map_cases, range_ord_iso_map_cases, well_ord_trichotomy

deleted bij_ss in favour of bij_inverse_ss

#! /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.