modifiers for classical wrappers operate on Proof.context instead of claset;

removed historic comments;

tuned exceptions -- avoid composing error messages in low-level situations;

tuned signature; tuned comments;

proper identifiers -- avoid crash of case translations;

reduced duplication

do not add case translation syntax in rep_datatype compatibility mode

run type inference on input to wrap_data

installed case translations in BNF package

tuned

more antiquotations;

tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side; declare command "print_case_translations" where it is actually defined;

updated keywords;

merged

merged

obsolete -- tools should refer to proper Proof.context;

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