src/HOL/Tools/res_atp_setup.ML
2005-12-14 mengj 2005-12-14 changed ATP input files' names and location.
2005-12-06 mengj 2005-12-06 Added more functions for new type embedding of HOL clauses.
2005-11-28 mengj 2005-11-28 Added in four control flags for HOL and FOL translations. Changed functions that perform HOL/FOL translations, and write ATP input to files. Removed some functions that are no longer needed.
2005-11-18 mengj 2005-11-18 -- added combinator reduction axioms (typed and untyped) for HOL goals. -- combined make_nnf functions for HOL and FOL goals. -- hypothesis of goals are now also skolemized by inference.
2005-11-09 paulson 2005-11-09 Skolemization by inference, but not quite finished
2005-11-03 mengj 2005-11-03 Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names. Also removed some functions that are not used any more.
2005-10-28 haftmann 2005-10-28 circumvented smlnj value restriction
2005-10-28 mengj 2005-10-28 Added new functions to handle HOL goals and lemmas. Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file. Removed several functions definitions, and combined them with those in other files.
2005-10-21 mengj 2005-10-21 Merged theory ResAtpOracle.thy into ResAtpMethods.thy
2005-10-19 mengj 2005-10-19 *** empty log message ***
2005-10-19 mengj 2005-10-19 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").