added min_elem, upto;

added value; simplified synchronized variable access;

simplified synchronized variable access; tuned;

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;