isabelle: File revisions

src/HOL/Tools/res_atp_methods.ML

Thu, 25 May 2006 11:52:33 +0200	mengj	A new "spass" method.	file \| diff \| annotate
Tue, 07 Mar 2006 03:49:26 +0100	mengj	When ATP methods call ATPs, all input clauses from one subgoal are written to one file.	file \| diff \| annotate
Thu, 23 Feb 2006 12:57:39 +0100	mengj	vampire/eprover methods can now be applied repeatedly until they fail.	file \| diff \| annotate
Sat, 21 Jan 2006 23:22:40 +0100	mengj	Ensure dereference is delayed.	file \| diff \| annotate
Thu, 19 Jan 2006 21:22:08 +0100	wenzelm	setup: theory -> theory;	file \| diff \| annotate
Mon, 28 Nov 2005 07:13:43 +0100	mengj	Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.	file \| diff \| annotate
Fri, 18 Nov 2005 07:06:07 +0100	mengj	-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.	file \| diff \| annotate
Fri, 28 Oct 2005 02:28:20 +0200	mengj	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
Wed, 19 Oct 2005 10:25:46 +0200	mengj	* empty log message *	file \| diff \| annotate
Wed, 19 Oct 2005 06:33:24 +0200	mengj	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