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;

clarified take/drop/chop prefix/suffix;

clarified signature;

proper signature (amending c4e9e0c50487);

tuned output;

tuned;

explicit graph for chains, which contains all nts as nodes;

tuned;

tuned;

prefer lazy update;

tuned output;

more operations;

include lemmas generally useful for combinatorial proofs

redundant;

allow cartouche within ML string;

verbatim output consists of plain lines;