| Thu, 23 Sep 2010 10:34:01 +0200 | blanchet | make SML/NJ happy | file | diff | annotate |
| Wed, 22 Sep 2010 10:02:39 +0200 | blanchet | make SML/NJ happier | file | diff | annotate |
| Tue, 21 Sep 2010 10:02:50 +0200 | blanchet | make SML/NJ happier | file | diff | annotate |
| Thu, 16 Sep 2010 15:16:08 +0200 | blanchet | refactoring: move ATP proof and error extraction code to "ATP_Proof" module | file | diff | annotate |
| Thu, 16 Sep 2010 14:24:48 +0200 | blanchet | avoid code duplication | file | diff | annotate |
| Thu, 16 Sep 2010 13:52:17 +0200 | blanchet | merge constructors | file | diff | annotate |
| Thu, 16 Sep 2010 13:44:41 +0200 | blanchet | factor out the inverse of "nice_atp_problem" | file | diff | annotate |
| Thu, 16 Sep 2010 11:59:45 +0200 | blanchet | use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs | file | diff | annotate |
| Thu, 16 Sep 2010 11:12:08 +0200 | blanchet | factored out TSTP/SPASS/Vampire proof parsing; | file | diff | annotate |