obua [Tue, 07 Mar 2006 16:03:31 +0100] rev 19203
Added HOL-ZF to Isabelle.
haftmann [Tue, 07 Mar 2006 14:09:48 +0100] rev 19202
substantial improvement in codegen iml
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.