| 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 |
| Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already | changeset | files |
| Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | instantiate induction rules automatically | changeset | files |