| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
don't slice if there are too few facts
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
nicer failure message when one-line proof reconstruction fails
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make all messages urgent in verbose mode
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize automatically even if Metis failed, if the external prover was really fast
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
fixed syntax of min options
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
better merging of similar outputs
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
update minimization documentation
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
imported patch sledge_doc_metis_as_prover
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
automatically minimize with Metis when this can be done within a few seconds
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize with Metis if possible
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
changeset |
files
|
| Mon, 30 May 2011 15:30:05 +0100 |
paulson |
Workaround for hyperref bug affecting index entries involving the | symbol
|
changeset |
files
|
| Mon, 30 May 2011 13:58:00 +0200 |
bulwahn |
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
|
changeset |
files
|
| Mon, 30 May 2011 13:57:59 +0200 |
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
|
| Mon, 30 May 2011 12:20:04 +0100 |
paulson |
merged multiple heads
|
changeset |
files
|
| Mon, 30 May 2011 12:15:17 +0100 |
paulson |
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
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
|
| Fri, 27 May 2011 21:11:44 +0200 |
krauss |
function tutorial: do not omit termination proof, even when discussing other things
|
changeset |
files
|
| Fri, 27 May 2011 16:45:24 +0200 |
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
|
| Fri, 27 May 2011 10:41:09 +0200 |
blanchet |
document new "try"
|
changeset |
files
|
| Fri, 27 May 2011 10:33:16 +0200 |
blanchet |
tuned comments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
new timeout section (cf. Nitpick manual)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
cleanup proof text generation code
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more Sledgehammer documentation updates
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor update
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
changeset |
files
|