haftmann [Wed, 08 Mar 2006 17:03:19 +0100] rev 19214
first running version of type classes
haftmann [Wed, 08 Mar 2006 16:29:07 +0100] rev 19213
first running version of type classes
paulson [Wed, 08 Mar 2006 10:19:57 +0100] rev 19212
Frequency strategy. Revised indentation, etc.
nipkow [Wed, 08 Mar 2006 10:06:31 +0100] rev 19211
*** empty log message ***
obua [Tue, 07 Mar 2006 18:02:11 +0100] rev 19210
added ROOT.ML
paulson [Tue, 07 Mar 2006 16:50:33 +0100] rev 19209
Indentation
paulson [Tue, 07 Mar 2006 16:49:48 +0100] rev 19208
Tidying and restructuring.
paulson [Tue, 07 Mar 2006 16:49:12 +0100] rev 19207
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
paulson [Tue, 07 Mar 2006 16:47:51 +0100] rev 19206
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
Removal of the unused err_list.
paulson [Tue, 07 Mar 2006 16:46:54 +0100] rev 19205
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson [Tue, 07 Mar 2006 16:45:04 +0100] rev 19204
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
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.
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;
wenzelm [Sat, 04 Mar 2006 21:10:09 +0100] rev 19185
tuned conj_curry;