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

only one theorem table for both code generators

proper default codegen attribute

tuned code setup

code generator more liberal with respect to sort constraints of instance parameters

more Isar for example

tuned funpow code generation

tuned min/max code generation

dropped superfluous if

tuned of_nat code generation

re-introduces axiom subst