moved future_scheduler flag to Concurrent/ROOT.ML;

added invalidate_group; SimpleThread.interrupt;

added fail-safe interrupt;

subject to Multithreading.enabled; raw_map: join sequentially, less overhead;

future result: Interrupt invalidates group, but pretends success otherwise;

added future_scheduler flag (tmp!), from skip_proofs.ML; added Concurrent/par_list_dummy.ML;

Dummy version of parallel list combinators -- plain sequential evaluation.

added Concurrent/par_list_dummy.ML;

improved performance of skolem cache, due to parallel map; misc tuning, less verbosity;

SimpleThread.interrupt;

report: back to single message;

added section label;

tuned

do logging to MASTERLOG centrally (avoid multiple writers over NFS as this tends to corrupt the log file if not mounted with -sync option which apparently is not the default any more).

removed legacy |>>>

established canonical argument order in SML code generators

established canonical argument order

made SMLNJ happy

less tracing; removed heartbeat thread;

Future.joint_results is already uninterruptible;

more careful handling of group interrupts; join control is uninterruptible; less tracing;

use polyml-cvs, which fixes a serious deadlock problem of Poly/ML runtime vs. GC;

added HOL-Main;

setmp_noncritical makes it work with future scheduler;

The result of the equality inference rule no longer undergoes factoring.

make the test for experimental sessions in isatest-check actually work (test for log files ending in e.log)

leave a log message when no snapshot is generated

clarified preprocessor policies

arbitrary is undefined

tuned whitespace