tuned AtpWrapper interfaces;

continued codegen tutorial

renamed AtpThread to AtpWrapper;

adding preferences is now permissive;

tuned;

adding preferences is now permissive, no error handling here; tuned messages;

CRITICAL access to preferences; tuned some interfaces;

export generic_pref etc.; CRITICAL access to preferences; misc cleanup, more conventional indentation;

renamed kill_all to kill, in conformance with atp_kill command; simplified/unified treatment of preferences; check_thread_manager: CRITICAL due to global ref; goal addressing via Thm.cprem_of; reduced NJ basis library stuff to bare minimum;

tuned comments;

added lemma

Added liveness analysis

info: back to plain printing; maintain state as Synchronized.var (cf. Pure/Concurrent/synchronized.ML); turned start into check_thread_manager, which forks the managing thread on demand; simplified heap operations; default preferences: only include e prover, which is most likely to be installed; misc simplifcation and tuning;

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;

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