| Fri, 20 Aug 2010 13:39:47 +0200 | blanchet | more fiddling with Sledgehammer's "add:" option | changeset | files |
| Fri, 20 Aug 2010 10:58:01 +0200 | blanchet | beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly); | changeset | files |
| Thu, 19 Aug 2010 19:34:11 +0200 | blanchet | generalize the "too general equality" code to handle facts like "x ~= A ==> x = B" | changeset | files |
| Thu, 19 Aug 2010 18:16:47 +0200 | blanchet | encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed | changeset | files |
| Thu, 19 Aug 2010 14:39:31 +0200 | blanchet | fix atomize | changeset | files |
| Thu, 19 Aug 2010 14:01:54 +0200 | blanchet | improve atomization | changeset | files |