simplified thread creation via SimpleThread;

simplified thread creation via SimpleThread; managing_thread: option type (fork of inactive thread assumes threads are available in the first place);

version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);

removed old/unused setup of raw ATP oracles;

tuned;

Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);

added PROOFGENERAL_EMACS, with attempt to find Carbon Emacs;

tuned tracing;

slower heartbeat;

added simple heartbeat thread;

time factor: one more digit;

more tuning of tracing messages;

include factor in timing report;

with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition; removed pointless comments;

tracing: ignore failure of any kind;

tuned SYNCHRONIZED: outermost Exn.release; tuned tracing;

program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;

added partiality section

corrected class antiquotation

max_threads_value always 1 for dummy version;

simplified Exn.EXCEPTIONS, flatten nested occurrences;

simplified Exn.EXCEPTIONS;

major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;

tuned

Yet another proof of Newman's lemma, this time using the coherent logic prover.

unit_source: more rigid parsing, stop after final qed;

excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context; tuned;

replaced can_defer by is_relevant (negation); future_proof: declare forked goal to prevent accidental generalization (e.g. instance goal);