mengj [Tue, 07 Mar 2006 03:58:50 +0100] rev 19197
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
mengj [Tue, 07 Mar 2006 03:56:59 +0100] rev 19196
Added functions to retrieve local and global atpset rules.
cnf thms to Term.term format.
mengj [Tue, 07 Mar 2006 03:54:11 +0100] rev 19195
Moved the settings for ATP time limit to res_atp.ML
mengj [Tue, 07 Mar 2006 03:51:40 +0100] rev 19194
Merged res_atp_setup.ML into res_atp.ML.
HOL translation is integrated with background Isabelle-ATP linkup.
Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.
mengj [Tue, 07 Mar 2006 03:49:26 +0100] rev 19193
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
mengj [Tue, 07 Mar 2006 03:48:02 +0100] rev 19192
Merged res_atp_setup.ML into res_atp.ML.
wenzelm [Sun, 05 Mar 2006 23:56:57 +0100] rev 19191
SELECT_GOAL: fixed trivial case;
webertj [Sun, 05 Mar 2006 18:49:13 +0100] rev 19190
fixed a typo in a comment
wenzelm [Sat, 04 Mar 2006 21:39:08 +0100] rev 19189
tuned;
wenzelm [Sat, 04 Mar 2006 21:10:12 +0100] rev 19188
method: SelectGoals;