| Thu, 01 Oct 2009 16:46:48 +0200 |
nipkow |
made spass additional default prover
|
changeset |
files
|
| Thu, 01 Oct 2009 16:43:19 +0100 |
paulson |
merged
|
changeset |
files
|
| Thu, 01 Oct 2009 16:42:53 +0100 |
paulson |
Proved a new theorem: nat_to_nat2_inj
|
changeset |
files
|
| Thu, 01 Oct 2009 15:54:55 +0200 |
boehmes |
turned unsynchronized ref into synchronized var
|
changeset |
files
|
| 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
|
| Thu, 01 Oct 2009 09:09:56 +0200 |
haftmann |
explicitly Unsynchronized
|
changeset |
files
|
| Thu, 01 Oct 2009 07:40:25 +0200 |
ballarin |
Merged.
|
changeset |
files
|
| Tue, 29 Sep 2009 22:15:54 +0200 |
ballarin |
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
|
changeset |
files
|
| Sun, 27 Sep 2009 11:50:27 +0200 |
ballarin |
Archive registrations by external view.
|
changeset |
files
|
| Sat, 26 Sep 2009 21:03:57 +0200 |
ballarin |
Stricter test: raise error if registration generates duplicate theorem.
|
changeset |
files
|
| Sat, 19 Sep 2009 18:43:11 +0200 |
ballarin |
Explicit management of registration mixins.
|
changeset |
files
|
| Wed, 19 Aug 2009 19:35:46 +0200 |
ballarin |
Improved comments and api names.
|
changeset |
files
|
| Thu, 01 Oct 2009 01:03:36 +0200 |
wenzelm |
eliminated dead code, redundant bindings and parameters;
|
changeset |
files
|
| Thu, 01 Oct 2009 00:32:00 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:49:53 +0200 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:44:23 +0200 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:30:37 +0200 |
wenzelm |
Sorts.of_sort_derivation: no pp here;
|
changeset |
files
|