1.1 --- a/TODO.md	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/TODO.md	Tue Apr 20 13:32:43 2021 +0200
     1.3 @@ -35,6 +35,12 @@
     1.4      >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
     1.5  
     1.6  
     1.7 -* more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations;
     1.8 +* WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
     1.9 +    - quite often "axiomatization ..." can be turned into "lemma ... by auto"
    1.10 +      without further ado;
    1.11 +    - sometimes this requires to use more specific types / type classes;
    1.12 +    - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
    1.13 +    - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
    1.14  
    1.15 -* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation;
    1.16 +* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
    1.17 +    - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");