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;

updated method "ferrack";

interpreter for List.append added again

quick_and_dirty (again) not touched anymore

require_thy: read_text *after* checking parents (otherwise outdating an existing descendant will leave the dependencies corrupted);

gen_add_inductive_i: treat abbrevs as local defs, expand by export; tuned;

tuned various Class interfaces; tuned;

removed obsolete Class.class_of_locale/locale_of_class;

tuned;