src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2011-05-30 ago fixed syntax of min options
2011-05-30 ago minimize with Metis if possible
2011-05-27 ago try both "metis" and (on failure) "metisFT" in replay
2011-05-27 ago prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
2011-05-27 ago handle non-auto try case of Sledgehammer better
2011-05-27 ago added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-27 ago renamed "Auto_Tools" "Try"
2011-05-27 ago renamed "metis_timeout" to "preplay_timeout" and continued implementation
2011-05-27 ago shorten minimizer command further, exploiting until-now-undocumented syntax
2011-05-27 ago added syntax for specifying Metis timeout (currently used only by SMT solvers)
2011-05-27 ago reintroduced Waldmeister but limit the number of remote threads created
2011-05-27 ago renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
2011-05-27 ago take out Waldmeister from default for now -- success rate too low on Judgment Day
2011-05-27 ago always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
2011-05-22 ago improved Waldmeister support -- even run it by default on unit equational goals
2011-05-13 ago reduce the number of mono iterations to prevent the mono code from going berserk
2011-05-13 ago added convenience syntax
2011-05-12 ago renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
2011-05-12 ago ensure that Auto Sledgehammer is run with full type information
2011-05-12 ago added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-05 ago smoother handling of ! and ? in type system names
2011-05-02 ago 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 ago 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 ago use ! for mildly unsound and !! for very unsound encodings
2011-05-01 ago implement the new ATP type system in Sledgehammer
2011-05-01 ago make sure the minimizer monomorphizes when it should
2011-05-01 ago added (without implementation yet) new type encodings for Sledgehammer/ATP
2011-04-21 ago tuning
2011-04-21 ago cleanup: get rid of "may_slice" arguments without changing semantics
2011-04-21 ago implemented general slicing for ATPs, especially E 1.2w and above
2011-04-16 ago modernized structure Proof_Context;
2011-04-05 ago renamed "const_args" option value to "args"
2011-04-05 ago killed unimplemented type encoding "preds"
2011-04-04 ago if "monomorphize" is enabled, mangle the type information in the names by default
2011-03-31 ago added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-02-08 ago available_provers ~> supported_provers (for clarity)
2011-01-08 ago misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-17 ago convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
2010-12-16 ago make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
2010-12-15 ago make "full_types" take precedence over "type_sys"
2010-12-15 ago implemented partially-typed "tags" type encoding
2010-12-15 ago 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 ago added "type_sys" option to Sledgehammer
2010-12-08 ago split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
2010-12-03 ago replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
2010-12-03 ago run synchronous Auto Tools in parallel
2010-11-18 ago enabled SMT solver in Sledgehammer by default
2010-11-10 ago 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 ago use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
2010-11-03 ago standardize on seconds for Nitpick and Sledgehammer timeouts
2010-10-26 ago integrated "smt" proof method with Sledgehammer
2010-10-26 ago tuning
2010-10-26 ago make SML/NJ happy
2010-10-25 ago make "sledgehammer_params" work on single-threaded platforms
2010-10-22 ago more robust handling of "remote_" vs. non-"remote_" provers
2010-10-22 ago fixed signature of "is_smt_solver_installed";
2010-10-22 ago took out "smt"/"remote_smt" from default ATPs until they are properly implemented
2010-10-22 ago make Sledgehammer minimizer fully work with SMT
2010-10-21 ago first step in adding support for an SMT backend to Sledgehammer
2010-10-21 ago use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."