| Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp) | changeset | files |
| Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | make it more likely that induction rules are picked up by Sledgehammer | changeset | files |
| Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | generalize the Vampire parser some more to cope with things like "{2, 3\}" seen in some proofs | changeset | files |