first step in sharing more code between ATP and Metis translation

more precise authorship, reflecting my own ignorance and hg annotate

generate raw induction rule as instance of generic rule with careful treatment of currying

generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type

admissibility on option type

also manage induction rule; tuned data slot

improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms

merged

Workaround for bug involving makeindex, hyperref and the | symbol

parameterize print_theorems over actual search function

added experimental yxml_find_theorems web service (but no client yet)

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