expandshort

ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext

domrange/image_subset,vimage_subset: deleted needless premise!
misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem

ind-syntax/rule_concl: recoded to avoid exceptions
intr-elim: now checks conclusions of introduction rules

func/fun_disjoint_Un: now uses ex_ex1I
list-fn/hd,tl,drop: new
simpdata/bquant_simps: new

list/list_case_type: restored!

bool.thy: changed 1 from a "def" to a translation
Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML

nat/succ_less_induct: new induction principle
arith/add_mono: new results about monotonicity

simpdata/mem_simps: removed the ones for succ and cons; added succI1,
consI2 to ZF_ss

upair/succ_iff: new, for use with simp_tac (cons_iff already existed)

ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ
nat/nat_0_in_succ: new

ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed

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