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

more Isar for example

tuned funpow code generation

tuned min/max code generation

dropped superfluous if

tuned of_nat code generation

re-introduces axiom subst

corrected SML undefined

updated to official version as of 07-Oct-2008;

fold_lines: more tuning, avoiding extra split_last;

extra check of PROOFGENERAL_HOME;

needs -b option for isabelle getenv

updated generated file;

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

renamed promise to future, tuned related interfaces;

more robust treatment of Interrupt (cf. exn.ML); future_schedule: group each theory separately;

more robust treatment of Interrupt; added release_all, release_first; proper signature;

more robust treatment of Interrupt (cf. exn.ML);

removed release_results (cf. Exn.release_all, Exn.release_first);

more precise join_futures, improved termination;