1.1 --- a/TODO.md	Mon Sep 13 15:42:43 2021 +0200
     1.2 +++ b/TODO.md	Mon Sep 13 16:01:48 2021 +0200
     1.3 @@ -53,10 +53,6 @@
     1.4      - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
     1.5      - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
     1.6  
     1.7 -* WN: eliminate ThmC.numerals_to_Free, check tests marked TOODOO.1
     1.8 -  + ? how do algebraic operations on numerals ? Presburger ? simplifier ? hack see
     1.9 -    https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
    1.10 -
    1.11  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
    1.12      takes only static arguments ----------------^^^^^^^^^^^^^^, not value of "hd_ord (f, g)"
    1.13      ? are there better approximations to old output of (*1*) than with (*2*)