src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-04 blanchet 2011-04-04 if "monomorphize" is enabled, mangle the type information in the names by default
2011-03-31 blanchet 2011-03-31 added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-02-09 blanchet 2011-02-09 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
2010-12-16 blanchet 2010-12-16 fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
2010-12-15 blanchet 2010-12-15 generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
2010-12-15 blanchet 2010-12-15 fix Vampire parsing problem
2010-12-15 blanchet 2010-12-15 added Sledgehammer support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
2010-12-15 blanchet 2010-12-15 implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
2010-11-26 blanchet 2010-11-26 put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-10-26 blanchet 2010-10-26 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-22 blanchet 2010-10-22 tuning
2010-10-22 blanchet 2010-10-22 compile
2010-10-22 blanchet 2010-10-22 fixed signature of "is_smt_solver_installed"; renaming
2010-10-22 blanchet 2010-10-22 renamed modules
2010-10-22 blanchet 2010-10-22 renamed files