| Tue, 30 Aug 2011 16:07:46 +0200 |
blanchet |
cleaner "pff" dummy TFF0 prover
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:46 +0200 |
blanchet |
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
added type abstractions (for declaring polymorphic constants) to TFF syntax
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
implement more of the polymorphic simply typed format TFF(1)
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
flip logic of boolean option so it's off by default
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
extended simple types with polymorphism -- the implementation still needs some work though
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
added dummy PFF prover, for debugging purposes
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:34 +0200 |
blanchet |
first step towards polymorphic TFF + changed defaults for Vampire
|
changeset |
files
|
| Tue, 30 Aug 2011 16:04:23 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 30 Aug 2011 14:29:39 +0200 |
nik |
removed explicit reliance on Hilbert_Choice.Eps
|
changeset |
files
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
improved handling of induction rules in Sledgehammer
|
changeset |
files
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
added generation of induction rules
|
changeset |
files
|