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 |