| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
minor doc adjustments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
make output more concise
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
merge timeout messages from several ATPs into one message to avoid clutter
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
mention contributions from LCP and explain metis and metisFT encodings
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fixed trivial fact detection
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
cleaner handling of equality and proxies (esp. for THF)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
recognize more ATP failures
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fully support all type system encodings in typed formats (TFF, THF)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
take out Waldmeister from default for now -- success rate too low on Judgment Day
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
document relevance filter a bit more
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
|
changeset |
files
|
| Thu, 26 May 2011 23:21:00 +0200 |
noschinl |
instance inat for complete_lattice
|
changeset |
files
|