| Thu, 12 May 2011 15:29:19 +0200 | blanchet | use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc. | changeset | files |
| Thu, 12 May 2011 15:29:19 +0200 | blanchet | further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up | changeset | files |