improve the natural formula relevance filter code, so that it behaves more like the CNF one

split SPASS time slot between SOS and non-SOS, in case SOS times out

yields ill-typed ATP/metis proofs -- raus!

make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"

merged

more direct definition simplifies proofs

merged

more precise tactic: do not escape to a different goal branch (REPEAT is still problematic, though)

a76ace919f1c wasn't quite right; second try

merge

never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts

better eta-expansion in Sledgehammer's clausification; make the eta-expansion code more robust in the face of polymorphic arguments + make eta-expansion happen more often, since it first-orderizes things

cosmetics

make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds

improve the new "natural formula" fact filter

explicit treatment of UTF8 sequences as Isabelle symbols;

ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);

escape UTF8 symbols for the ML compiler;

explicit treatment of UTF8 character sequences as Isabelle symbols;

slight cleaning and simplification of the automatic wrapper for quotient definitions

merged

export of proper information in the ML-interface of the quotient package

treat Pretty.T as strictly abstract type;

slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;

avoid equality on abstract type Pretty.T;

notes on packaging;

misc tuning;

tuned auxiliary structures;

Net.encode_type;

more accurate dependencies;

made smlnj happy

fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem

renamed for easier grep

use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code

steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs

have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry

fix bug with "skolem_id" + sort facts for increased readability

if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again

merged

this looks like the most appropriate place to do the beta-eta-contraction

killed legacy "neg_clausify" and "clausify"

merged

factor out TPTP format output into file of its own, to facilitate further changes

merged

turn on "natural form" filtering in the Mirabelle tests, to see how it performs

missing "Unsynchronized" + make exception take a unit

added code to optionally perform fact filtering on the original (non-CNF) formulas

more cosmetics

cosmetics + prevent consideration of inlined Skolem terms in relevance filter

canonical argument order

leverage new data structure for handling "add:" and "del:"

thread original theorem along with CNF theorem, as a step toward killing the Skolem cache

merge "generic_prover" and "generic_tptp_prover"

removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.

distinguish between "unknown" and "no Kodkodi installed" errors

reintroduce new Sledgehammer polymorphic handling code; this time I tested the proper version of Isabelle