document new type system syntax

use ! for mildly unsound and !! for very unsound encodings

use new type system syntax

implement the new ATP type system in Sledgehammer

define type system in ATP module so that ATPs can suggest a type system

made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support

merge symbol declarations that are type-instances of each other -- useful for type system "Args true" with monomorphization turned off

drop even more bound types in symbol declarations -- useful in particular for type system "Args true"

tuning

got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly

drop "fequal" type args for unmangled type systems

recognize more SystemOnTPTP errors

cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0

make sure that fequal keeps its type arguments for mangled type systems

no needless "fequal" proxies if "explicit_apply" is set + always have readable names

shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs

avoid Type.TYPE_MATCH exception for "True_or_False" for "If"

proper handling of partially applied proxy symbols

make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type

improve helper type instantiation code

killed needless datatype "combtyp" in Metis

have properly type-instantiated helper facts (combinators and If)

don't destroy sym table entry for special symbols such as "hAPP" if "explicit_apply" is set

better known failure recognition for ToFoF-E