Mon, 26 Jul 2010 17:17:59 +0200 | blanchet | kill Skolem handling in Sledgehammer | changeset | files |
Mon, 26 Jul 2010 17:09:10 +0200 | blanchet | simplify "conjecture_shape" business, as a result of using FOF instead of CNF | changeset | files |
Mon, 26 Jul 2010 17:03:21 +0200 | blanchet | generate full first-order formulas (FOF) in Sledgehammer | changeset | files |