isabelle: File revisions

src/HOL/Tools/res_atp_methods.ML

2006-05-25	mengj	2006-05-25	A new "spass" method.	file \| diff \| annotate
2006-03-07	mengj	2006-03-07	When ATP methods call ATPs, all input clauses from one subgoal are written to one file.	file \| diff \| annotate
2006-02-23	mengj	2006-02-23	vampire/eprover methods can now be applied repeatedly until they fail.	file \| diff \| annotate
2006-01-21	mengj	2006-01-21	Ensure dereference is delayed.	file \| diff \| annotate
2006-01-19	wenzelm	2006-01-19	setup: theory -> theory;	file \| diff \| annotate
2005-11-28	mengj	2005-11-28	Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. Still have old verions of "vampireH","vampireF", "eproverH", "eproverF", which can be called to handle HOL or FOL problems.	file \| diff \| annotate
2005-11-18	mengj	2005-11-18	-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.	file \| diff \| annotate
2005-10-28	mengj	2005-10-28	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.	file \| diff \| annotate
2005-10-19	mengj	2005-10-19	* empty log message *	file \| diff \| annotate
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").	file \| diff \| annotate

isabelle