even -> evn because even is now in Main

dropped redundant transfer rules (now proved and registered by datatype and plugins)

proper context for typedef;

proper proof context for typedef;

proper context;

proper context for match_tac etc.;

proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

avoid erule and rotated in IMP

reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility

self-contained simp rules for dvd on numerals

equivalence rules for structures without zero divisors

removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);

optional proof context for unify operations, for the sake of proper local options;

clarified name of Type.unified, to emphasize its connection to the "unify" family; tuned low-level operation;

proper Envir.norm_type for result of Type.raw_unifys;

avoid slow metis proof;

proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);

tuned;

updated some sledgehammer proofs -- much faster;

updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);

recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54); NB: "match" operates on direct substitution without variable chasing, in contrast to "unify" (and Unify.matches!) which work on cascaded env;

more direct type equality;

reverted commit accident from 994fe0ba8335

less space-wasting serialization setup: highest cell of array has been unused so far

tuned outline;

tuned syntax -- separate tokens;

eliminated pointless check -- command definitions are subject to theory context;

merged

prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors; tuned message;

tuned markup;