generic ScgiServer.simple_handler

moved html templates to a separate module, making their awkward signatures explicit

attempt to clarify code; removed "handle _" and dead code

(de)serialization for search query and result

explicit type for search queries

moved questionable goal modification out of filter_theorems

exported raw query parser; removed inconsistent clone

separate query parsing from actual search

fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other

document new explicit apply

made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly

don't slice if there are too few facts

nicer failure message when one-line proof reconstruction fails

make SML/NJ happy

avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples

make all messages urgent in verbose mode

minimize automatically even if Metis failed, if the external prover was really fast

fixed syntax of min options

no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout

better merging of similar outputs

update minimization documentation

imported patch sledge_doc_metis_as_prover

automatically minimize with Metis when this can be done within a few seconds

minimize with Metis if possible

support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing

Workaround for hyperref bug affecting index entries involving the | symbol

improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of

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

merged multiple heads

Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler

always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated

normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages

function tutorial: do not omit termination proof, even when discussing other things

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

document new "try"

tuned comments

new timeout section (cf. Nitpick manual)

cleanup proof text generation code

more Sledgehammer documentation updates

minor update

try both "metis" and (on failure) "metisFT" in replay

show time taken for reconstruction

unbreak "max_potential" logic

more concise output

compile

use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)

repaired theory merging and defined/used helpers

make Sledgehammer a little bit less verbose in "try"

handle non-auto try cases gracefully in Try Methods

handle non-auto try case gracefully in Solve Direct

prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators

update SML section of documentation

handle non-auto try case gracefully in Nitpick

handle non-auto try case of Sledgehammer better

added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods

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

renamed "Auto_Tools" "Try"

removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP

renamed "try" "try_methods"

renamed "metis_timeout" to "preplay_timeout" and continued implementation