store external accesses within name space (as produced by naming policy); improved sticky_prefix: suppress redundant accesses to achieve shorter output; removed unused interfaces; replaced accesses' by external_names (depening on naming);

removed unused set_policy;

replaced NameSpace.accesses' by NameSpace.external_names (depening on naming);

added sorted_list_of_set

tuned fork_mixfix (back from class.ML);

clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');

removed obsolete fork_mixfix (back to theory_target.ML);

updated;

clarified fork_mixfix

exported standard_term_check

global class syntax

added yield_singleton

Syntax.(un)check: explicit result option;

apply_wrappers: perhaps_apply/loop;

added perhaps_apply/loop;

Mark A. Hillebrand, DFKI: Robust sub/superscripts in LaTeX document output.

updated;

DeclareRobustCommand isascriptstyle (enables sub/superscripts within section headings etc.);

tuned Const.the_abbreviation;

misc cleanup of abbrev/local_const;

added revert_abbrev; contract_abbrevs: ignore Syntax.internalM (changed meaning of this special case); print_abbrevs: proper treatment of global consts (after local/global swap);

add_bind: close_schematic_term;

tuned hidden_polymorphism; added close_schematic_term;

add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again); added revert_abbrev;

the_abbreviation: return plain rhs only; force_expand: expand to plain rhs; added revert_abbrev; tuned;

added the "max_sledgehammers" option

Fixed variable naming in mutual induction rules

"sequential" is no longer a keyword. It is still used as before, but as a normal identifier => no pollution of keyword space

polished some comments

unparse_arity: unparse type constructor as well;