| Fri, 05 Dec 2008 17:26:16 -0800 |
huffman |
add lemma le_nat_number_of
|
changeset |
files
|
| Sat, 06 Dec 2008 12:18:05 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 06 Dec 2008 08:57:39 +0100 |
haftmann |
adapted to changes in binding module
|
changeset |
files
|
| Sat, 06 Dec 2008 08:45:38 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
changeset |
files
|
| Fri, 05 Dec 2008 18:42:39 +0100 |
haftmann |
corrected theory path
|
changeset |
files
|
| Fri, 05 Dec 2008 18:42:37 +0100 |
haftmann |
removed Table.extend, NameSpace.extend_table
|
changeset |
files
|
| Sat, 06 Dec 2008 00:09:01 +0100 |
wenzelm |
renamed force_proof to join_proof;
|
changeset |
files
|
| Sat, 06 Dec 2008 00:08:32 +0100 |
wenzelm |
renamed force_proofs to join_proofs;
|
changeset |
files
|
| Sat, 06 Dec 2008 00:08:07 +0100 |
wenzelm |
finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
|
changeset |
files
|
| Sat, 06 Dec 2008 00:04:44 +0100 |
wenzelm |
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
|
changeset |
files
|
| Sat, 06 Dec 2008 00:03:28 +0100 |
wenzelm |
excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
|
changeset |
files
|