prefer control symbol antiquotations;

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

@{command_spec} is superseded by @{command_keyword};

Thm.cterm_of and Thm.ctyp_of operate on local context;

clarified context;

tuned signature -- prefer qualified names;

prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;

modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
proper context for global data;
tuned signature;

tuned signature;

eliminated clone of Inductive.mk_cases_tac;

tuned signature;

tuned whitespace;

provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);

tuned signature;

more explicit exception pattern (NB: unqualified exceptions without arguments are in danger of becoming catch-all patterns by accident);

distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
some notes about missing ML interface;

tuned white space;
avoid "object-oriented English";

dropped unnecessary 'open'

tuned headers

generate elim rules for elimination of function equalities;
added fun_cases command;
recover proper cases rules for mutual recursive case (no sum types)