Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
pass more facts to LEO-II, in the light of latest evaluation
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
prevent an "Empty" exception (e.g. with Satallax, "mono_native")
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
tuning terminology
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
updated NEWS
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
updated docs
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
added "args_query" encodings
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
removed killed encodings from Metis examples
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
updated docs
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
killed most unsound encodings
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
generalized monotonic constructor optimisation so that it works with e.g. the product type
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
removed micro-optimization whose justification I can't recall
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
add missing timeout multiplier
|
changeset |
files
|
Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
avoid dumping definitions several times in LEO-II proofs
|
changeset |
files
|