fixed random number invocation

make sure E type information constants are given a weight, even if they don't appear anywhere else

fix ROOT.ML and handle "readable_names" reference slightly more cleanly

show sorts not just types in Isar proofs + tuning

Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses -- parse these correctly

tuning

make SML/NJ happy

added TPTP exporter facility -- useful to do experiments with machine learning

renamed theory to make its purpose clearer

fixing typo

improving naming of fresh variables in OCaml serializer

adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)

merged;

modernized rail diagrams using @{rail} antiquotation;

tuning

fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs

use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...

beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)

minor doc fixes

adapt to new type system names

restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"

take "partial_types" option with a grain of salt

fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings

close formula universally, to make SPASS happy

fixed embarrassing bug where conjecture and fact offsets were swapped

pick up GaveUp error on SystemOnTPTP

avoid trailing digits for SNARK (type) names -- grr...

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

cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation

fixed min-arity computation when "explicit_apply" is specified

fixed "tags" type encoding after latest round of changes

more higher-order tests for Sledgehammer/ATP

added friendly hint when Isar proof is missing

fix handling of proxies after recent drastic changes to the type encodings

added a hint to Metis errors suggesting metisFT -- it sometimes work

reconstruct TFF type predicates correctly for ToFoF

fixed parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y))

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)