src/HOL/Tools/res_atp_methods.ML
2006-05-25 ago A new "spass" method.
2006-03-07 ago When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
2006-02-23 ago vampire/eprover methods can now be applied repeatedly until they fail.
2006-01-21 ago Ensure dereference is delayed.
2006-01-19 ago setup: theory -> theory;
2005-11-28 ago Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
2005-11-18 ago -- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
2005-10-28 ago Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
2005-10-19 ago *** empty log message ***
2005-10-19 ago Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").