| Mon, 29 Sep 2008 12:31:58 +0200 |
haftmann |
separate HOL-Main image
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:57 +0200 |
haftmann |
polished code generator setup
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:56 +0200 |
haftmann |
added theory antiquotation
|
changeset |
files
|
| Mon, 29 Sep 2008 11:46:52 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Mon, 29 Sep 2008 11:46:47 +0200 |
wenzelm |
handle _ should be avoided (spurious Interrupt will spoil the game);
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:04 +0200 |
wenzelm |
added norm_export_morphism;
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:03 +0200 |
wenzelm |
added exit_global, exit_result, exit_result_global;
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:01 +0200 |
wenzelm |
LocalTheory.exit_global;
|
changeset |
files
|
| Sun, 28 Sep 2008 14:46:51 +0200 |
wenzelm |
HOL no longer depends on HOL-Plain;
|
changeset |
files
|
| Sun, 28 Sep 2008 14:40:43 +0200 |
wenzelm |
setmp_noncritical;
|
changeset |
files
|
| Sun, 28 Sep 2008 12:42:35 +0200 |
wenzelm |
join earlier promises first;
|
changeset |
files
|
| Sun, 28 Sep 2008 12:23:45 +0200 |
wenzelm |
proper setmp_thread_data for nested execute (cf. join_loop);
|
changeset |
files
|
| Sun, 28 Sep 2008 12:23:44 +0200 |
wenzelm |
promise_result: enforce strictly sequential dependencies, via serial numbers;
|
changeset |
files
|
| Sun, 28 Sep 2008 09:25:24 +0200 |
kleing |
do not cvs update for doc test (switching to mercurial, update done outside
|
changeset |
files
|
| Sun, 28 Sep 2008 09:13:46 +0200 |
kleing |
use mercurial repository for isatest
|
changeset |
files
|
| Sun, 28 Sep 2008 00:00:55 +0200 |
wenzelm |
thread_data: include thread name, export access;
|
changeset |
files
|
| Sat, 27 Sep 2008 19:35:00 +0200 |
wenzelm |
setmp_noncritical;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:08 +0200 |
wenzelm |
dequeue_towards: return bound for unfinished tasks;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:07 +0200 |
wenzelm |
moved release_results to future.ML;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:06 +0200 |
wenzelm |
added release_results (formerly in par_list.ML);
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:05 +0200 |
wenzelm |
Future.release_results;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:37:01 +0200 |
wenzelm |
more tracing;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:39 +0200 |
wenzelm |
Theory.checkpoint for main operations, admits concurrent proofs;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:37 +0200 |
wenzelm |
promise: include check into future body, i.e. joined results are always valid;
|
changeset |
files
|