| Tue, 26 Jul 2011 18:11:38 +0200 |
bulwahn |
more precise dependencies
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
further worked around LEO-II parser limitation, with eta-expansion
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
no need for existential witnesses for sorts in TFF and THF formats
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
mangle "undefined"
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
tuning -- remove useless function (at this point combinators are already in)
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
remove spurious message
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
|
changeset |
files
|
| Tue, 26 Jul 2011 14:50:15 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Tue, 26 Jul 2011 14:05:28 +0200 |
Andreas Lochbihler |
fixed code generator setup in List_Cset
|
changeset |
files
|
| Tue, 26 Jul 2011 13:50:03 +0200 |
hoelzl |
enat is a complete_linorder instance
|
changeset |
files
|
| Tue, 26 Jul 2011 12:44:36 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|