State variables with synchronized access.

added generic combinator for synchronized evaluation (formerly in future.ML);

simplified implementation using Synchronized.var;

SimpleThread.synchronized;

added Concurrent/synchronized.ML;

** Update from Fabian ** added remote prover functions;

** Update from Fabian ** reset print mode when producing proof text;

** Update from Fabian ** preferences/provers: separated by white space, avoid low-level char type; sledgehammer command accepts prover list as well; avoid I/O in critical section of AtpManager.info; more systematic synchronization using higher-order combinators; more descriptive errors when atp fails; keep explicitly requested problem files; added remote prover functions; simplified treatment of prover name in diagnostic output; misc tuning and cleanup;

tuned output;

tuned

tuned

change DISTPREFIX to not use yet another filesystem

tuned

tuned

tuned

tuned

`code func` now just `code`

some adaption

using tikz pictures

tuned default rules of (dvd)

replaced str_of by general peek;

extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;

fixed spelling;

added enabled; removed pseudo-parallel version of profile -- CRITICAL prevents future join;

added enabled;

Multithreading.enabled;

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

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