src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
2010-12-15 blanchet 2010-12-15 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
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 "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
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-12-15 blanchet 2010-12-15 added "type_sys" option to Sledgehammer
2010-12-08 blanchet 2010-12-08 implicitly call the minimizer for SMT solvers that don't return an unsat core
2010-12-08 blanchet 2010-12-08 clarified terminology
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-26 blanchet 2010-10-26 no need to encode theorem number twice in skolem names
2010-10-22 blanchet 2010-10-22 tuning
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