src/HOL/Tools/ATP/atp_problem.ML
2010-09-16 blanchet 2010-09-16 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs
2010-09-16 blanchet 2010-09-16 factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"
2010-09-15 blanchet 2010-09-15 in debug mode, don't touch "$true" and "$false"
2010-09-02 blanchet 2010-09-02 fix bug in "debug" mode
2010-08-22 blanchet 2010-08-22 prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible; the disjunctive view of "conjecture" is nonstandard but taken by E, SPASS, Vampire, etc.
2010-08-20 blanchet 2010-08-20 use "hypothesis" rather than "conjecture" for hypotheses in TPTP format; avoids relying on inconsistently implemented feature of TPTP format
2010-08-17 blanchet 2010-08-17 more parentheses in TPTP formulas, just in case
2010-07-29 blanchet 2010-07-29 fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
2010-07-28 blanchet 2010-07-28 consequence of directory renaming
2010-07-28 blanchet 2010-07-28 rename directory