tuned isabelle usage;

updated generated file;

simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;

updated generated file;

replaced ISABELLE by ISABELLE_PROCESS;

ISABELLE_PROCESS commandline;

replaced ISATOOL by ISABELLE_TOOL;

ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL -- old bindings stay for a while (legacy feature);

eliminated prompt messages;

added isabelle_tool version as basic integrity check of platform/distribution;

renamed isatool to isabelle_tool in programming interfaces;

Theory header keywords.

added Thy/thy_header.scala;

tuned quotes;

factor: proper padding of digits;

plain process_id function;

removed obsolete Posix/Signal compatibility wrappers;

removed obsolete Posix/Signal compatibility wrappers; plain process_id function; adapted to recent changes in Pure;

removed obsolete Posix/Signal compatibility wrappers; plain process_id function;

do not handle Error (which matches arbitrary exceptions!), but ERROR _;

updated to new AtpManager;

operate on Proof.state, not Toplevel.state; moved setup to ATP_Linkup.thy;

misc simplifcation and tuning; no export of structure Provers; added add_provers, print_provers; operate on Proof.state, not Toplevel.state; use Time.+ etc. to make SML/XL of NJ happy; explicit Isar commands 'atp_kill', 'atp_info', 'print_atps';

perform atp_setups here;

updated generated file;

removed HOL-Plain -- already included in HOL;

removed spurious ResAtp.set_prover;

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);

datatype transition: internal trans field is maintained in reverse order; tuned;

future_proof: protect conclusion of deferred proof state;

future_schedule: back to one group for all loader tasks;

tuned comments;

fixed