mengj [Tue, 07 Mar 2006 04:06:02 +0100] rev 19201
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
The hash table (for removing duplicate) now stores clauses as Term.term with names.
mengj [Tue, 07 Mar 2006 04:04:21 +0100] rev 19200
relevance_filter takes input axioms as Term.term.
mengj [Tue, 07 Mar 2006 04:01:25 +0100] rev 19199
Proof reconstruction now only takes names of theorems as input.
mengj [Tue, 07 Mar 2006 03:59:48 +0100] rev 19198
Added tptp_write_file to write all necessary ATP input clauses to one file.
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;
wenzelm [Sat, 04 Mar 2006 21:10:11 +0100] rev 19187
method: syntax for SelectGoals;
wenzelm [Sat, 04 Mar 2006 21:10:10 +0100] rev 19186
text: added SelectGoals;