| 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 |