| Tue, 07 Mar 2006 16:50:33 +0100 |
paulson |
Indentation
|
changeset |
files
|
| Tue, 07 Mar 2006 16:49:48 +0100 |
paulson |
Tidying and restructuring.
|
changeset |
files
|
| Tue, 07 Mar 2006 16:49:12 +0100 |
paulson |
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
|
changeset |
files
|
| Tue, 07 Mar 2006 16:47:51 +0100 |
paulson |
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
|
changeset |
files
|
| Tue, 07 Mar 2006 16:46:54 +0100 |
paulson |
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
|
changeset |
files
|
| Tue, 07 Mar 2006 16:45:04 +0100 |
paulson |
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
|
changeset |
files
|
| Tue, 07 Mar 2006 16:03:31 +0100 |
obua |
Added HOL-ZF to Isabelle.
|
changeset |
files
|
| Tue, 07 Mar 2006 14:09:48 +0100 |
haftmann |
substantial improvement in codegen iml
|
changeset |
files
|
| Tue, 07 Mar 2006 04:06:02 +0100 |
mengj |
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
|
changeset |
files
|
| Tue, 07 Mar 2006 04:04:21 +0100 |
mengj |
relevance_filter takes input axioms as Term.term.
|
changeset |
files
|
| Tue, 07 Mar 2006 04:01:25 +0100 |
mengj |
Proof reconstruction now only takes names of theorems as input.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:59:48 +0100 |
mengj |
Added tptp_write_file to write all necessary ATP input clauses to one file.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:58:50 +0100 |
mengj |
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:56:59 +0100 |
mengj |
Added functions to retrieve local and global atpset rules.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:54:11 +0100 |
mengj |
Moved the settings for ATP time limit to res_atp.ML
|
changeset |
files
|
| Tue, 07 Mar 2006 03:51:40 +0100 |
mengj |
Merged res_atp_setup.ML into res_atp.ML.
|
changeset |
files
|
| 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.
|
changeset |
files
|
| Tue, 07 Mar 2006 03:48:02 +0100 |
mengj |
Merged res_atp_setup.ML into res_atp.ML.
|
changeset |
files
|
| Sun, 05 Mar 2006 23:56:57 +0100 |
wenzelm |
SELECT_GOAL: fixed trivial case;
|
changeset |
files
|
| Sun, 05 Mar 2006 18:49:13 +0100 |
webertj |
fixed a typo in a comment
|
changeset |
files
|
| Sat, 04 Mar 2006 21:39:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:12 +0100 |
wenzelm |
method: SelectGoals;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:11 +0100 |
wenzelm |
method: syntax for SelectGoals;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:10 +0100 |
wenzelm |
text: added SelectGoals;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:09 +0100 |
wenzelm |
tuned conj_curry;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:08 +0100 |
wenzelm |
added extract, retrofit;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:07 +0100 |
wenzelm |
added mk_conjunction;
|
changeset |
files
|
| Sat, 04 Mar 2006 21:10:06 +0100 |
wenzelm |
method: restriction to first n sub-goals;
|
changeset |
files
|
| Fri, 03 Mar 2006 19:43:46 +0100 |
nipkow |
minor changes
|
changeset |
files
|
| Fri, 03 Mar 2006 19:30:30 +0100 |
nipkow |
more examples
|
changeset |
files
|