updated keywords;

localized and modernized adhoc-overloading (patch by Christian Sternagel);

merged

tuned proof;

reraise interrupts outside command regular transactions -- relevant for memo_stable;

added "isabelle update_sub_sup" tool;

allow spaces in file names; tuned;

more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;

added |>! and #>! for convenient printing of timing information

preplay failures might be resolved later, so proceed as usual

more reasonable preplay_interface semantics

tuned

minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps

merged

clarified memo_exec: plain synchronized access without any special tricks;

tuned;

clarified execution: maintain running execs only, check "stable" separately via memo (again); tuned signatures;

tuned signature; tuned comments;

clarified module name;

more explicit type Exec.context; eliminated obsolete execution group -- NB: cancelation happens individually for registered execs;

tuned signature; unified exceptions for this module;

strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;

tuned -- cleanup before publishing assignment;

more abstract types; tuned signature;

tuned;

disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution; tuned error messages: prefer plain "error" as in document.ML;

more precise fact declarations -- fewer warnings;

global management of command execution fragments; tuned;

fully synchronized guard of running execution; tuned;

merged