ML name space -- dummy version of Poly/ML 5.2 facility.

added ML-Systems/ml_name_space.ML;

use ML_prf within proofs;

local @{context};

moved global ML bindings to global place;

back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;

updated generated file;

wf_finite_psubset[simp], in_finite_psubset[simp]

Public interface to interpretation morphism.

moved term_of syntax to separate theory

removed obsolete theory

added quickcheck.ML

tuned comments;

multithreading for Poly/ML 5.1 is no longer supported;

tuned;

updated system manual;

Proof General / Emacs interface wrapper;

Proof General: option -I is obsolete;

added PROOFGENERAL_HOME;

separate emacs tool for Proof General / Emacs;

added quickcheck stub

removed babel again

celver code lemma avoid type ambiguity problem with Haskell

a sophisticated char/nibble conversion combinator

moved term_of syntax to separate theory

SimpleThread.fork;

Simplified thread fork interface.

added Concurrent/simple_thread.ML;

updated generated file;

misc tuning and modernization;

check setting and tool; added file;

Clearer separation of interpretation frontend and backend.

No interpretation of locale with dangling type frees.

Do not rely on locale assumption in interpretation.

The metis method now fails in the usual manner, rather than raising an exception, if it determines that it cannot prove the theorem.

Fixed typo in locale declaration.

added babel

explicit size of characters

dropped superfluous code lemmas

evaluation using code generator

generic value command

converted symbols.tex;

tuned;

converted misc.tex;

tuned;

generated files;

converted present.tex;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

load underscore package after iman etc.;

tuned comment;

added formal markup for setting, executable, tool;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

converted basics.tex to theory file;

added isatt markup;

New outline for codegen tutorial -- draft

added extern_fact (local or global); more procise printing of fact names;

print raw (internal) result names;

more procise printing of fact names;

pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;

cancel, shutdown: notify_all;

finish: Future.shutdown last;

eliminated requests, use global state variables uniformly; more robust shutdown;

finish: Future.shutdown;

added is_empty;

shutdown: global join-and-shutdown operation; reduced trace_active; scheduler_fork: always notify; tracing for thread exit; unique ids for workers;

added focus, which indicates a particular collection of high-priority tasks; tuned;

some general notes on future values;

separate Concurrent/ROOT.ML;

Parallel list combinators.

added Concurrent/par_list.ML;

added interrupt_task (external id); tuned signature;

tuned;

future_schedule: uninterruptible join;

added future_scheduler (default false);

replaced join_all by join_results, which returns Exn.results; join: disallow Multithreading.self_critical, which is prone to deadlocks due to context change via fork;

workers: explicit activity flag; SYNCHRONIZED: optional tracing;

future: allow explicit group; cancel: invalidate group identifier for all future members; tuned comments; tuned;

cancel: invalidate group implicitly, via bool ref; job: moved ok flag into group; added interrupt, interrupt_external for tasks;

auto_flush: uniform block buffering for all output streams;

auto_flush stdout, stderr as well;

proper values of no_interrupts, regular_interrupts;

cancel: check_scheduler; adapted to simplified TaskQueue.cancel; improved join/join_all: actively work towards results, i.e. do not yield unnecessarily; misc tuning;

simplified dequeue: provide Thread.self internally; simplified cancel: interrupt running threads internally; added depend; added dequeue_towards; misc tuning;

eliminated cache, access queue efficiently via IntGraph.get_first;

export get_first from underlying table;

out_stream: block-buffered, with separate autoflush thread (every 50ms);

babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;

added comment

human-readable printing of TaskQueue.task/group;

* Changed defaults for unify configuration options;

inherit group from running thread, or create a new one -- make it harder to re-use canceled groups; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;

job: explicit 'ok' status -- false for canceled jobs; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;

Overall exception handler in order to insulate our users from low-level bugs.

more careful exception handling in order to prevent backtracking; miscellaneous tidying up.

Increasing the default limits in order to prevent unnecessary failures.

send: broadcast condition while locked!

proper signature constraint;

tuned Mailbox.send;

removed unused sync_interrupts;

moved thread data to future.ML (again); dequeue: include group; more interrupt operations; misc tuning;

more interrupt operations; maintain thread data (formerly in task_queue.ML); wait: added tracing; added requests mailbox; handle excessive workers fork: inherit group; added rudimentary shutdown; misc tuning;

moved task, thread_data, group, queue to task_queue.ML; tuned signature; SYNCHRONIZED notify_all! misc tuning;

Ordered queue of grouped tasks. formerly in future.ML; added thread data; added group; more robust dequeue: change into running here; misc tuning;

added Concurrent/task_queue.ML;

await: SYNCHRONIZED wait!

tuned check_cache; removed broken self_synchronized, which cannot be used in conjunction with condition variables; more precise use of SYNCHRONIZED vs. wait; tuned worker_loop;

added sync_interrupts, regular_interrupts; max_thread_value: enforce >= 1;

added sync_interrupts, regular_interrupts;

opaque signature constraint abstracts local type abbrev;

tuned;

added change_result;

Functional threads as future values.

added Concurrent/future.ML;

Default (mostly dummy) implementation of thread structures. formerly in multithreading.ML; create mutexes / condition variables without failure;

*** MESSAGE REFERS TO PREVIOUS VERSION *** removed dummy thread structures from multithreading.ML;

*** empty log message ***

explicit use of universal.ML and dummy_thread.ML;

added no_interrupts; tuned;

added no_interrupts; moved dummy thread structures to dummy_thread.ML;

tuned;