| Mon, 29 Sep 2008 21:26:44 +0200 |
wenzelm |
install_pp Future.T (polyml only);
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:41 +0200 |
wenzelm |
report_token/parse_token: back to context-less version;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:39 +0200 |
wenzelm |
back to plain Position.report for regular references;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:36 +0200 |
wenzelm |
back to plain Position.report for regular references;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:32 +0200 |
wenzelm |
promise global proofs;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:26 +0200 |
wenzelm |
renamed report to report_visible;
|
changeset |
files
|
| Mon, 29 Sep 2008 14:59:02 +0200 |
wenzelm |
code example: back to individual ML commands, which are now thread-safe;
|
changeset |
files
|
| Mon, 29 Sep 2008 14:41:25 +0200 |
wenzelm |
ContextPosition.report;
|
changeset |
files
|
| Mon, 29 Sep 2008 14:41:24 +0200 |
wenzelm |
target update: invisible context position avoids duplication of reports etc.;
|
changeset |
files
|
| Mon, 29 Sep 2008 14:41:23 +0200 |
wenzelm |
Context position visibility.
|
changeset |
files
|
| Mon, 29 Sep 2008 14:41:22 +0200 |
wenzelm |
added context_position.ML;
|
changeset |
files
|
| Mon, 29 Sep 2008 12:32:00 +0200 |
haftmann |
more precise redundancy check
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:59 +0200 |
haftmann |
clarified dependencies between arith tools
|
changeset |
files
|
| 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
|