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

make the Nitpick_Example theory processable even when Kodkodi is not installed; so that at least the "theory" aspects of it (as opposed to the diagnosis offered by Nitpick) are checked on everybody's machines

Make latex happy

Quotient package now uses Partial Equivalence instead place of equivalence

Replace 'list_rel' by 'list_all2'; they are equivalent.

Proper treatment of non-inherited mixins.

merged

Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.

reredisable new polymorphic code

merged

beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later; reintroduced old proof based on Metis, since it was a good test for the Skolemizer

back to post-release mode;

merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;

make Nitpick's unsound mode a bit more unsound

sort cases on the proper key

compile

thread "full_types"

try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better

clean up after fcc768dc9dd0

adjusted Nitpick examples to latest changes + make them slightly faster

optimized code generated for datatype cases + more; more = lazy creation of debugging messages in mono code + use of "let" when performing some beta-applications (to avoid exponential blowup) + removal of some set constructs, to simplify the code and increase precision in some cases (and decrease it in others, but this can be regained)

activated Scala code generator test

added bot instances; tuned

extensionality rule fset_eqI

merged

separate section for diagnostic commands

more binding; avoid arcane Rep and Abs prefixes

cleanup of typecopy package

quickcheck for fsets

merged

added pigeonhole lemmas

merged

tuned whitespace; dropped dead code

code_simp: only succeed on real progress

prefer fold over foldl

conclude simplification with default simpset

drop subsumed default equations (requires a little bit unfortunate laziness)

avoid Scala legacy operations

prefer fold over foldl