| 2011-05-31 |
blanchet |
added new metis mode, with no implementation yet
|
changeset |
files
|
| 2011-05-31 |
blanchet |
tuning
|
changeset |
files
|
| 2011-05-31 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
changeset |
files
|
| 2011-05-31 |
krauss |
more precise authorship, reflecting my own ignorance and hg annotate
|
changeset |
files
|
| 2011-05-31 |
krauss |
generate raw induction rule as instance of generic rule with careful treatment of currying
|
changeset |
files
|
| 2011-05-31 |
krauss |
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
|
changeset |
files
|
| 2011-05-31 |
krauss |
admissibility on option type
|
changeset |
files
|
| 2011-05-23 |
krauss |
also manage induction rule;
|
changeset |
files
|
| 2011-05-30 |
bulwahn |
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
|
changeset |
files
|
| 2011-05-30 |
paulson |
merged
|
changeset |
files
|
| 2011-05-30 |
paulson |
Workaround for bug involving makeindex, hyperref and the | symbol
|
changeset |
files
|
| 2011-05-30 |
krauss |
parameterize print_theorems over actual search function
|
changeset |
files
|
| 2011-05-30 |
krauss |
added experimental yxml_find_theorems web service (but no client yet)
|
changeset |
files
|
| 2011-05-30 |
krauss |
generic ScgiServer.simple_handler
|
changeset |
files
|
| 2011-05-30 |
krauss |
moved html templates to a separate module, making their awkward signatures explicit
|
changeset |
files
|
| 2011-05-30 |
krauss |
attempt to clarify code; removed "handle _" and dead code
|
changeset |
files
|
| 2011-05-30 |
krauss |
(de)serialization for search query and result
|
changeset |
files
|
| 2011-05-30 |
krauss |
explicit type for search queries
|
changeset |
files
|
| 2011-05-30 |
krauss |
moved questionable goal modification out of filter_theorems
|
changeset |
files
|
| 2011-05-30 |
krauss |
exported raw query parser; removed inconsistent clone
|
changeset |
files
|
| 2011-05-30 |
krauss |
separate query parsing from actual search
|
changeset |
files
|
| 2011-05-30 |
blanchet |
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
|
changeset |
files
|
| 2011-05-30 |
blanchet |
document new explicit apply
|
changeset |
files
|
| 2011-05-30 |
blanchet |
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
|
changeset |
files
|
| 2011-05-30 |
blanchet |
don't slice if there are too few facts
|
changeset |
files
|
| 2011-05-30 |
blanchet |
nicer failure message when one-line proof reconstruction fails
|
changeset |
files
|
| 2011-05-30 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| 2011-05-30 |
blanchet |
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
|
changeset |
files
|
| 2011-05-30 |
blanchet |
make all messages urgent in verbose mode
|
changeset |
files
|
| 2011-05-30 |
blanchet |
minimize automatically even if Metis failed, if the external prover was really fast
|
changeset |
files
|
| 2011-05-30 |
blanchet |
fixed syntax of min options
|
changeset |
files
|
| 2011-05-30 |
blanchet |
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
|
changeset |
files
|
| 2011-05-30 |
blanchet |
better merging of similar outputs
|
changeset |
files
|
| 2011-05-30 |
blanchet |
update minimization documentation
|
changeset |
files
|
| 2011-05-30 |
blanchet |
imported patch sledge_doc_metis_as_prover
|
changeset |
files
|
| 2011-05-30 |
blanchet |
automatically minimize with Metis when this can be done within a few seconds
|
changeset |
files
|
| 2011-05-30 |
blanchet |
minimize with Metis if possible
|
changeset |
files
|
| 2011-05-30 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
changeset |
files
|
| 2011-05-30 |
paulson |
Workaround for hyperref bug affecting index entries involving the | symbol
|
changeset |
files
|
| 2011-05-30 |
bulwahn |
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
|
changeset |
files
|
| 2011-05-30 |
bulwahn |
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
|
changeset |
files
|
| 2011-05-30 |
paulson |
merged multiple heads
|
changeset |
files
|
| 2011-05-30 |
paulson |
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
|
changeset |
files
|
| 2011-05-29 |
blanchet |
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
|
changeset |
files
|
| 2011-05-29 |
blanchet |
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
|
changeset |
files
|
| 2011-05-27 |
krauss |
function tutorial: do not omit termination proof, even when discussing other things
|
changeset |
files
|
| 2011-05-27 |
boehmes |
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
|
changeset |
files
|
| 2011-05-27 |
blanchet |
document new "try"
|
changeset |
files
|
| 2011-05-27 |
blanchet |
tuned comments
|
changeset |
files
|
| 2011-05-27 |
blanchet |
new timeout section (cf. Nitpick manual)
|
changeset |
files
|
| 2011-05-27 |
blanchet |
cleanup proof text generation code
|
changeset |
files
|
| 2011-05-27 |
blanchet |
more Sledgehammer documentation updates
|
changeset |
files
|
| 2011-05-27 |
blanchet |
minor update
|
changeset |
files
|
| 2011-05-27 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
changeset |
files
|
| 2011-05-27 |
blanchet |
show time taken for reconstruction
|
changeset |
files
|
| 2011-05-27 |
blanchet |
unbreak "max_potential" logic
|
changeset |
files
|
| 2011-05-27 |
blanchet |
more concise output
|
changeset |
files
|
| 2011-05-27 |
blanchet |
compile
|
changeset |
files
|
| 2011-05-27 |
blanchet |
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
|
changeset |
files
|
| 2011-05-27 |
blanchet |
repaired theory merging and defined/used helpers
|
changeset |
files
|