handle special constants correctly in Isar proof reconstruction code, especially type predicates

make sure the minimizer monomorphizes when it should

fixed arity of special constants if "explicit_apply" is set

make sure typing fact names are unique (needed e.g. by SNARK)

minor cleanup

reimplemented the hAPP introduction code so that it's done earlier, when the types are still available

declare TFF types so that SNARK can be used with types

perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it

move type declarations to the front, for TFF-compliance

use postfix syntax for mangled types, for consistency with unmangled

generate typing for "hBOOL" in "Many_Typed" mode + tuning

generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)

improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work

unprefix evil "fof_" prefix inserted by ToFoF

added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format

fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged

generate TFF type declarations in typed mode

no point in keeping indices in Sledgehammer readable var names, since these are disambiguated anyway

added more rudimentary type support to Sledgehammer's ATP encoding

fixed type of ATP quantifier types (sic)

added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS

added support for TFF type declarations

reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter

added room for types in ATP quantifiers