2011-05-30 krauss 2011-05-30 separate query parsing from actual search
2011-05-30 blanchet 2011-05-30 fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
2011-05-30 blanchet 2011-05-30 document new explicit apply
2011-05-30 blanchet 2011-05-30 made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
2011-05-30 blanchet 2011-05-30 don't slice if there are too few facts
2011-05-30 blanchet 2011-05-30 nicer failure message when one-line proof reconstruction fails
2011-05-30 blanchet 2011-05-30 make SML/NJ happy
2011-05-30 blanchet 2011-05-30 avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
2011-05-30 blanchet 2011-05-30 make all messages urgent in verbose mode
2011-05-30 blanchet 2011-05-30 minimize automatically even if Metis failed, if the external prover was really fast
2011-05-30 blanchet 2011-05-30 fixed syntax of min options
2011-05-30 blanchet 2011-05-30 no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
2011-05-30 blanchet 2011-05-30 better merging of similar outputs
2011-05-30 blanchet 2011-05-30 update minimization documentation
2011-05-30 blanchet 2011-05-30 imported patch sledge_doc_metis_as_prover
2011-05-30 blanchet 2011-05-30 automatically minimize with Metis when this can be done within a few seconds
2011-05-30 blanchet 2011-05-30 minimize with Metis if possible
2011-05-30 blanchet 2011-05-30 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
2011-05-30 paulson 2011-05-30 Workaround for hyperref bug affecting index entries involving the | symbol
2011-05-30 bulwahn 2011-05-30 improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
2011-05-30 bulwahn 2011-05-30 automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
2011-05-30 paulson 2011-05-30 merged multiple heads
2011-05-30 paulson 2011-05-30 Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
2011-05-29 blanchet 2011-05-29 always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
2011-05-29 blanchet 2011-05-29 normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
2011-05-27 krauss 2011-05-27 function tutorial: do not omit termination proof, even when discussing other things
2011-05-27 boehmes 2011-05-27 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
2011-05-27 blanchet 2011-05-27 document new "try"
2011-05-27 blanchet 2011-05-27 tuned comments
2011-05-27 blanchet 2011-05-27 new timeout section (cf. Nitpick manual)
2011-05-27 blanchet 2011-05-27 cleanup proof text generation code
2011-05-27 blanchet 2011-05-27 more Sledgehammer documentation updates
2011-05-27 blanchet 2011-05-27 minor update
2011-05-27 blanchet 2011-05-27 try both "metis" and (on failure) "metisFT" in replay
2011-05-27 blanchet 2011-05-27 show time taken for reconstruction
2011-05-27 blanchet 2011-05-27 unbreak "max_potential" logic
2011-05-27 blanchet 2011-05-27 more concise output
2011-05-27 blanchet 2011-05-27 compile
2011-05-27 blanchet 2011-05-27 use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
2011-05-27 blanchet 2011-05-27 repaired theory merging and defined/used helpers
2011-05-27 blanchet 2011-05-27 make Sledgehammer a little bit less verbose in "try"
2011-05-27 blanchet 2011-05-27 handle non-auto try cases gracefully in Try Methods
2011-05-27 blanchet 2011-05-27 handle non-auto try case gracefully in Solve Direct
2011-05-27 blanchet 2011-05-27 prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
2011-05-27 blanchet 2011-05-27 update SML section of documentation
2011-05-27 blanchet 2011-05-27 handle non-auto try case gracefully in Nitpick
2011-05-27 blanchet 2011-05-27 handle non-auto try case of Sledgehammer better
2011-05-27 blanchet 2011-05-27 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-27 blanchet 2011-05-27 removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
2011-05-27 blanchet 2011-05-27 renamed "Auto_Tools" "Try"
2011-05-27 blanchet 2011-05-27 removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
2011-05-27 blanchet 2011-05-27 renamed "try" "try_methods"
2011-05-27 blanchet 2011-05-27 renamed "metis_timeout" to "preplay_timeout" and continued implementation
2011-05-27 blanchet 2011-05-27 minor fixes to Sledgehammer docs
2011-05-27 blanchet 2011-05-27 shorten minimizer command further, exploiting until-now-undocumented syntax
2011-05-27 blanchet 2011-05-27 minor tweaks to the Nitpick documentation
2011-05-27 blanchet 2011-05-27 added syntax for specifying Metis timeout (currently used only by SMT solvers)
2011-05-27 blanchet 2011-05-27 readded Waldmeister as default to the documentation and other minor changes
2011-05-27 blanchet 2011-05-27 reintroduced Waldmeister but limit the number of remote threads created
2011-05-27 blanchet 2011-05-27 renamed "minimize" to "min" to make Sledgehammer output a little bit more concise