Handle dummy patterns in parse translation rather than check phase

disallow coercions to interfere with case translations

allow redundant cases in the list comprehension translation

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

no need to filter tautologies anymore -- they are prefiltered by "all_facts"'

work on CASC LTB ISA exporter

tuning

add continuous_on rules for products

fixed spelling

move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative

remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

improved printing of exception CTERM (see also d0f0f37ec346);

prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);

more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;

discontinued odd magic number, which was once used for performance measurements;

document @{make_string}, cf. NEWS of Isabelle2009-2 (June 2010);

merged

more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;

try to preserve original linearization

use somewhat lighter encoding

robustness w.r.t. unknown arguments

cleaned

cleaned

tuned

tuned signature -- agree with markup terminology;

unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;

tuned document

tuned

sup on multisets

convenient induction rule

tuned README -- less buzzwords;