| Thu, 01 Oct 2009 15:19:49 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 01 Oct 2009 15:19:23 +0200 |
nipkow |
resolved conflict
|
changeset |
files
|
| Thu, 01 Oct 2009 11:35:13 +0200 |
nipkow |
record max lemmas used
|
changeset |
files
|
| Thu, 01 Oct 2009 18:24:06 +0200 |
wenzelm |
Lazy evaluation with memoing (sequential version).
|
changeset |
files
|
| Thu, 01 Oct 2009 18:21:11 +0200 |
wenzelm |
more official status of sequential implementations;
|
changeset |
files
|
| Thu, 01 Oct 2009 18:10:41 +0200 |
wenzelm |
separate concurrent/sequential versions of lazy evaluation;
|
changeset |
files
|
| Thu, 01 Oct 2009 16:27:13 +0200 |
wenzelm |
added Task_Queue.depend (again) -- light-weight version for transitive graph;
|
changeset |
files
|
| Thu, 01 Oct 2009 16:09:47 +0200 |
wenzelm |
handle Pattern.MATCH, not arbitrary exceptions;
|
changeset |
files
|
| Thu, 01 Oct 2009 16:03:43 +0200 |
wenzelm |
more precise dependencies;
|
changeset |
files
|
| Thu, 01 Oct 2009 15:44:42 +0200 |
wenzelm |
eliminated redundant parameters;
|
changeset |
files
|
| Thu, 01 Oct 2009 14:27:50 +0200 |
wenzelm |
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
|
changeset |
files
|
| Thu, 01 Oct 2009 14:11:28 +0200 |
wenzelm |
avoid mixed l/r infixes, which do not work in some versions of SML;
|
changeset |
files
|
| Thu, 01 Oct 2009 12:15:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Oct 2009 11:33:32 +0200 |
wenzelm |
merged
|
changeset |
files
|