discontinued obsolete ML antiquotation @{claset};

added ML antiquotation @{theory_context};

more standard module name Axclass (according to file name);

made SML/NJ happy

generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector

NEWS and CONTRIBUTORS

declaration attribute for case combinators

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;