Changes

Summary

1. tuned data structure: potentially more efficient add_prods;
2. clarified operations;
3. merged
4. expand definitions of \DeclareOldFontCommand in traditional article.cls, e.g. KOMA-Script no longer provides these;
5. irrelevant reference to doubtful theory Code_Char
6. avoid concrete (anti)mono in theorem names since it could be the other way round
7. more uniform documentation;
8. proper fall-back rendering of control symbol;