recur in the expression to be matched (do not rely on repetitive execution of a check phase); separate ML-interface function that is not recurring (strip_case)

tuned whitespace

Use Type.raw_match instead of Sign.typ_match

special constant to prevent eta-contraction of the check-phase syntax of case translations

separate data used for case translation from the datatype package

case translations performed in a separate check phase (with adjustments by traytel)

formal proof context for axclass proofs; avoid global_simpset_of -- refer to simpset of proof context;

prefer local context;

proper proof context; removed historic comments;

tuned;

merged

add command timings (like document command status);

tuned signature;

public Isabelle_Process.xml_cache (thread-safe); cache derived status messages;

tuned signature;

just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;

clarified protocol_message undefinedness;

quote by Alan Kay;

more accurate documentation;

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;

more accurate documentation of "(structure)" mixfix;

more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;

tuned comment;

just one syntax category "mixfix" -- check structure annotation semantically;

tuned message;

handle case clashes on Mac file system by encoding goal numbers

avoid duplicate "tcon_" names

smoothly handle cyclic graphs

compile + fixed naming convention

reverted accidental changes to theory file + updated wrt ML file