1.1 --- a/TODO.md	Mon Aug 09 11:19:25 2021 +0200
     1.2 +++ b/TODO.md	Mon Aug 09 14:20:20 2021 +0200
     1.3 @@ -63,10 +63,10 @@
     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, DONE partially;
     1.8 -  + TOODOO are exclusive for this changeset; most follow from TOODOO.1
     1.9 -  + TOODOO.1: exception TYPE raised by Skip_Proof.make_thm 
    1.10 -  + ? how to do algebraic operations on numerals ? Presburger ? simplifier ?
    1.11 +* WN: eliminate ThmC.numerals_to_Free, done except 1 error:
    1.12 +  + exception TYPE raised by Skip_Proof.make_thm, several inherited errors in tests marked TOODOO.1
    1.13 +  + ? how do algebraic operations on numerals ? Presburger ? simplifier ? hack see
    1.14 +    https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
    1.15  
    1.16  * WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
    1.17        Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)