src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
2011-06-10 blanchet 2011-06-10 pass --trim option to "eproof" script to speed up proof reconstruction
2011-06-09 blanchet 2011-06-09 cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
2011-06-09 blanchet 2011-06-09 added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)
2011-06-08 blanchet 2011-06-08 exploit new semantics of "max_new_instances"
2011-06-08 blanchet 2011-06-08 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
2011-06-08 blanchet 2011-06-08 killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
2011-06-07 blanchet 2011-06-07 prioritize more relevant facts for monomorphization
2011-06-07 blanchet 2011-06-07 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
2011-06-07 blanchet 2011-06-07 workaround current "max_new_instances" semantics
2011-06-07 blanchet 2011-06-07 move away from old SMT monomorphizer
2011-06-07 blanchet 2011-06-07 merged
2011-06-07 blanchet 2011-06-07 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
2011-06-07 blanchet 2011-06-07 removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
2011-06-07 blanchet 2011-06-07 nicely thread monomorphism verbosity in Metis and Sledgehammer
2011-06-07 boehmes 2011-06-07 clarified meaning of monomorphization configuration option by renaming it
2011-06-07 blanchet 2011-06-07 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-07 blanchet 2011-06-07 use new monomorphization code
2011-06-07 blanchet 2011-06-07 renamed ML function
2011-06-07 blanchet 2011-06-07 pass props not thms to ATP translator
2011-06-06 blanchet 2011-06-06 removed confusing slicing logic
2011-06-06 blanchet 2011-06-06 suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
2011-06-06 blanchet 2011-06-06 effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
2011-06-06 blanchet 2011-06-06 removed old optimization that isn't one anyone
2011-06-06 blanchet 2011-06-06 Metis code cleanup
2011-06-06 blanchet 2011-06-06 enable new Metis
2011-06-06 blanchet 2011-06-06 more preparations towards hijacking Metis
2011-06-06 blanchet 2011-06-06 remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
2011-06-06 blanchet 2011-06-06 make "metisX"'s default more like old "metis"
2011-06-06 blanchet 2011-06-06 temporarily added "MetisX" as reconstructor and minimizer
2011-06-06 blanchet 2011-06-06 show what failed to play
2011-06-01 blanchet 2011-06-01 tuned names
2011-05-31 blanchet 2011-05-31 tuned name
2011-05-31 blanchet 2011-05-31 make "prepare_atp_problem" more robust w.r.t. choice of type system
2011-05-31 blanchet 2011-05-31 don't preprocess twice
2011-05-31 blanchet 2011-05-31 more work on new metis that exploits the powerful new type encodings
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-05-30 blanchet 2011-05-30 don't slice if there are too few facts
2011-05-30 blanchet 2011-05-30 automatically minimize with Metis when this can be done within a few seconds
2011-05-30 blanchet 2011-05-30 minimize with Metis if possible
2011-05-30 blanchet 2011-05-30 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
2011-05-29 blanchet 2011-05-29 always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
2011-05-27 blanchet 2011-05-27 cleanup proof text generation code
2011-05-27 blanchet 2011-05-27 try both "metis" and (on failure) "metisFT" in replay
2011-05-27 blanchet 2011-05-27 show time taken for reconstruction
2011-05-27 blanchet 2011-05-27 more concise output
2011-05-27 blanchet 2011-05-27 handle non-auto try case of Sledgehammer better
2011-05-27 blanchet 2011-05-27 renamed "metis_timeout" to "preplay_timeout" and continued implementation
2011-05-27 blanchet 2011-05-27 added syntax for specifying Metis timeout (currently used only by SMT solvers)
2011-05-27 blanchet 2011-05-27 make output more concise
2011-05-27 blanchet 2011-05-27 merge timeout messages from several ATPs into one message to avoid clutter
2011-05-27 blanchet 2011-05-27 fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
2011-05-27 blanchet 2011-05-27 fully support all type system encodings in typed formats (TFF, THF)
2011-05-27 blanchet 2011-05-27 towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
2011-05-24 blanchet 2011-05-24 respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")
2011-05-24 blanchet 2011-05-24 more work on parsing LEO-II proofs and extracting uses of extensionality
2011-05-24 blanchet 2011-05-24 slightly gracefuller handling of LEO-II and Satallax output
2011-05-24 blanchet 2011-05-24 identify HOL functions with THF functions
2011-05-24 blanchet 2011-05-24 started adding support for THF output (but no lambdas)
2011-05-24 blanchet 2011-05-24 filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
2011-05-24 blanchet 2011-05-24 tuning -- the "appropriate" terminology is inspired from TPTP