src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2011-05-12 blanchet 2011-05-12 renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
2011-05-12 blanchet 2011-05-12 ensure that Auto Sledgehammer is run with full type information
2011-05-12 blanchet 2011-05-12 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-05 blanchet 2011-05-05 smoother handling of ! and ? in type system names
2011-05-02 blanchet 2011-05-02 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
2011-05-01 blanchet 2011-05-01 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
2011-05-01 blanchet 2011-05-01 use ! for mildly unsound and !! for very unsound encodings
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-05-01 blanchet 2011-05-01 make sure the minimizer monomorphizes when it should
2011-05-01 blanchet 2011-05-01 added (without implementation yet) new type encodings for Sledgehammer/ATP
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