src/HOL/Tools/ATP/atp_problem.ML
Thu, 16 Sep 2010 11:59:45 +0200 blanchet use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
Thu, 16 Sep 2010 11:12:08 +0200 blanchet factored out TSTP/SPASS/Vampire proof parsing;
Wed, 15 Sep 2010 10:26:09 +0200 blanchet in debug mode, don't touch "$true" and "$false"
Thu, 02 Sep 2010 22:49:56 +0200 blanchet fix bug in "debug" mode
Sun, 22 Aug 2010 09:43:10 +0200 blanchet prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
Fri, 20 Aug 2010 15:16:27 +0200 blanchet use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
Tue, 17 Aug 2010 16:46:43 +0200 blanchet more parentheses in TPTP formulas, just in case
Thu, 29 Jul 2010 16:11:02 +0200 blanchet fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
Wed, 28 Jul 2010 19:04:59 +0200 blanchet consequence of directory renaming
Wed, 28 Jul 2010 19:01:34 +0200 blanchet rename directory
less more (0) tip