1.1 --- a/TODO.md	Fri May 07 18:12:51 2021 +0200
     1.2 +++ b/TODO.md	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -29,11 +29,16 @@
     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, use existing Isabelle/HOL representation
     1.8 -    - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
     1.9 +* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation, DONE partially;
    1.10 +    - TODO: ? how to do algebraic operations on numerals ? Presburger ? simplifier ?
    1.11 +    - TODO: clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
    1.12  
    1.13 -* WN: Part.DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art);
    1.14 +* WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
    1.15        Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
    1.16        Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
    1.17  
    1.18  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
    1.19 +      ???
    1.20 +
    1.21 +* WN: reduce the number of TermC.parse*;
    1.22 +    - one or two variants should suffice.