src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2011-04-21 blanchet 2011-04-21 tuning
2011-04-21 blanchet 2011-04-21 cleanup: get rid of "may_slice" arguments without changing semantics
2011-04-21 blanchet 2011-04-21 implemented general slicing for ATPs, especially E 1.2w and above
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-05 blanchet 2011-04-05 renamed "const_args" option value to "args"
2011-04-05 blanchet 2011-04-05 killed unimplemented type encoding "preds"
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-08 blanchet 2011-02-08 available_provers ~> supported_provers (for clarity)
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-17 blanchet 2010-12-17 convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
2010-12-16 blanchet 2010-12-16 make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
2010-12-15 blanchet 2010-12-15 make "full_types" take precedence over "type_sys"
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-12-15 blanchet 2010-12-15 added "type_sys" option to Sledgehammer
2010-12-08 blanchet 2010-12-08 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
2010-12-03 blanchet 2010-12-03 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
2010-12-03 blanchet 2010-12-03 run synchronous Auto Tools in parallel
2010-11-18 blanchet 2010-11-18 enabled SMT solver in Sledgehammer by default
2010-11-10 wenzelm 2010-11-10 use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);
2010-11-03 blanchet 2010-11-03 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; updated docs
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-10-26 blanchet 2010-10-26 integrated "smt" proof method with Sledgehammer
2010-10-26 blanchet 2010-10-26 tuning
2010-10-26 blanchet 2010-10-26 make SML/NJ happy
2010-10-25 blanchet 2010-10-25 make "sledgehammer_params" work on single-threaded platforms
2010-10-22 blanchet 2010-10-22 more robust handling of "remote_" vs. non-"remote_" provers
2010-10-22 blanchet 2010-10-22 fixed signature of "is_smt_solver_installed"; renaming
2010-10-22 blanchet 2010-10-22 took out "smt"/"remote_smt" from default ATPs until they are properly implemented
2010-10-22 blanchet 2010-10-22 make Sledgehammer minimizer fully work with SMT
2010-10-21 blanchet 2010-10-21 first step in adding support for an SMT backend to Sledgehammer
2010-10-21 blanchet 2010-10-21 use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
2010-09-13 blanchet 2010-09-13 use 30 s instead of 60 s as the default Sledgehammer timeout; very few proofs are lost this way (esp. thanks to the parallel use of provers, cf. Boehme & Nipkow 2010), and this is much more tolerable for users
2010-09-11 blanchet 2010-09-11 tuning
2010-09-11 blanchet 2010-09-11 finished renaming "Auto_Counterexample" to "Auto_Tools"
2010-09-11 blanchet 2010-09-11 implemented Auto Sledgehammer
2010-09-01 blanchet 2010-09-01 got rid of the "theory_relevant" option; instead, have fudge factors that behave more smoothly for all provers
2010-09-01 blanchet 2010-09-01 generalize theorem argument parsing syntax
2010-08-31 blanchet 2010-08-31 finished renaming
2010-08-31 blanchet 2010-08-31 added "expect" feature of Nitpick to Sledgehammer, for regression testing
2010-08-31 blanchet 2010-08-31 added "blocking" option to Sledgehammer to run in synchronous mode; sometimes useful, e.g. for testing
2010-08-31 blanchet 2010-08-31 add a penalty for being higher-order
2010-08-30 blanchet 2010-08-30 make Sledgehammer's relevance filter somewhat slacker
2010-08-25 blanchet 2010-08-25 reorganize options regarding to the relevance threshold and decay
2010-08-25 blanchet 2010-08-25 make relevance filter work in term of a "max_relevant" option + use Vampire SOS; "max_relevant" is more reliable than "max_relevant_per_iter"; also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before; SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)
2010-08-25 blanchet 2010-08-25 get rid of "defs_relevant" feature; nobody uses it and it works poorly
2010-08-25 blanchet 2010-08-25 renamed "relevance_convergence" to "relevance_decay"
2010-08-23 blanchet 2010-08-23 invert semantics of "relevance_convergence", to make it more intuitive
2010-08-23 blanchet 2010-08-23 if no facts were selected on first iteration, try again with a lower threshold
2010-08-18 blanchet 2010-08-18 get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
2010-08-18 blanchet 2010-08-18 added "max_relevant_per_iter" option to Sledgehammer
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-07-29 blanchet 2010-07-29 use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses
2010-07-28 blanchet 2010-07-28 minor refactoring
2010-07-28 blanchet 2010-07-28 minor refactoring
2010-07-27 blanchet 2010-07-27 minor refactoring
2010-07-27 blanchet 2010-07-27 rename "ATP_Manager" ML module to "Sledgehammer"; more refactoring to come
2010-07-21 blanchet 2010-07-21 renamings + only need second component of name pool to reconstruct proofs
2010-06-28 blanchet 2010-06-28 always perform "inline" skolemization, polymorphism or not, Skolem cache or not