| Thu, 16 Sep 2010 14:24:48 +0200 | blanchet | avoid code duplication | changeset | files |
| Thu, 16 Sep 2010 14:24:03 +0200 | blanchet | tuning | changeset | files |
| Thu, 16 Sep 2010 13:52:17 +0200 | blanchet | merge constructors | changeset | files |
| Thu, 16 Sep 2010 13:44:41 +0200 | blanchet | factor out the inverse of "nice_atp_problem" | changeset | files |
| Thu, 16 Sep 2010 11:59:45 +0200 | blanchet | use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs | changeset | files |
| Thu, 16 Sep 2010 11:12:08 +0200 | blanchet | factored out TSTP/SPASS/Vampire proof parsing; | changeset | files |
| Thu, 16 Sep 2010 09:59:32 +0200 | blanchet | prevent exception when calling "Mirabelle.can_apply" on empty proof sequence; | changeset | files |