more operations;

prefer specific tokens_subtract: subtle change of comparison via tokens_match;

tuned type: absorb NONE: token option as token_none: token;

tuned;

clarified types and operations: potentially more efficient add_prods; tuned data structure;

clarified modules; tuned;

tuned: more explicit types;

tuned data structure: potentially more efficient add_prods;

clarified operations;

merged

expand definitions of \DeclareOldFontCommand in traditional article.cls, e.g. KOMA-Script no longer provides these;

irrelevant reference to doubtful theory Code_Char

avoid concrete (anti)mono in theorem names since it could be the other way round

more uniform documentation;

proper fall-back rendering of control symbol;