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;

renamed Consts.the_declaration to Consts.the_type;

renamed the_declaration to the_type; added type_scheme, which covers proper consts and abbreviations (like typargs); tuned;

tuned

swapped constant components

canonical interpretation interface

prefer first constant component on merge

explicit parameter for class finite

tuned comment;

more on authentic syntax;