| 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
|
| Tue, 26 Jul 2011 10:49:34 +0200 |
Andreas Lochbihler |
Add theory for setting up monad syntax for Cset
|
changeset |
files
|
| Tue, 26 Jul 2011 11:48:11 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 26 Jul 2011 08:07:01 +0200 |
bulwahn |
removing expectations from quickcheck example
|
changeset |
files
|
| Tue, 26 Jul 2011 08:07:00 +0200 |
bulwahn |
adding remarks after static inspection of the invocation of the SML code generator
|
changeset |
files
|