mechanism to keep SMT input and output files around in Mirabelle

proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction

added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)

enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day

Cygwin: Poly/ML 5.4.0 requires libgmp3;

updated to polyml-5.4.0;

tuned;

updated for Poly/ML 5.4.0;

merged

avoid ML structure aliases (especially single-letter abbreviations)

added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions

merged

configure domain package to work with HOL option type

make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction

simplify proofs

beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction

configure domain package to work with HOL sum type

replace list_map function with an abbreviation

merged

run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy

disable feature that was enabled by mistake

make exceptions more transparent in "debug" mode

remove spurious line

use the options provided by Stephan Schulz -- much better

optionally supply constant weights to E -- turned off by default until properly parameterized

merged

type_lifting for predicates

proper identifiers for consts and types;

some attempts to fit diagnostic output into regular TTY (75-80 characters per line);

tuned/clarified some component settings; explicit comments about common mistakes;