1.1 --- a/TODO.md	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/TODO.md	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -36,6 +36,4 @@
     1.4        Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
     1.5        Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
     1.6  
     1.7 -* WN: simplify const names like "is'_expanded": no need to imitate the escape of mixfix syntax;
     1.8 -
     1.9  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};