| Tue, 31 Jan 2012 14:39:21 +0100 |
blanchet |
new SPASS setup
|
changeset |
files
|
| Tue, 31 Jan 2012 12:43:48 +0100 |
blanchet |
distinguish between ":lr" and ":lt" (terminating) in DFG format
|
changeset |
files
|
| Tue, 31 Jan 2012 10:29:05 +0100 |
blanchet |
nicer keyword class avoidance scheme
|
changeset |
files
|
| Tue, 31 Jan 2012 10:29:04 +0100 |
blanchet |
new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)
|
changeset |
files
|
| Tue, 31 Jan 2012 09:06:27 +0100 |
bulwahn |
mutabelle must handle the case where quickcheck returns multiple results
|
changeset |
files
|
| Tue, 31 Jan 2012 08:52:47 +0100 |
blanchet |
reverted e2b1a86d59fc -- broke Metis's lambda-lifting
|
changeset |
files
|
| Tue, 31 Jan 2012 07:11:20 +0100 |
nipkow |
merged
|
changeset |
files
|
| Tue, 31 Jan 2012 07:11:04 +0100 |
nipkow |
NEWS
|
changeset |
files
|
| Mon, 30 Jan 2012 21:49:41 +0100 |
nipkow |
added "'a rel"
|
changeset |
files
|
| Mon, 30 Jan 2012 22:56:09 +0100 |
blanchet |
fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers
|
changeset |
files
|
| Mon, 30 Jan 2012 17:18:58 +0100 |
blanchet |
new SPASS setup
|
changeset |
files
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
example tuning
|
changeset |
files
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
implemented new lambda translations scheme
|
changeset |
files
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
avoid unsupported case in Metis
|
changeset |
files
|