1.1 --- a/TODO.md	Mon Jul 19 18:29:46 2021 +0200
     1.2 +++ b/TODO.md	Mon Jul 19 18:39:02 2021 +0200
     1.3 @@ -67,7 +67,6 @@
     1.4    + TOODOO are exclusive for this changeset; most follow from TOODOO.1
     1.5    + TOODOO.1: exception TYPE raised by Skip_Proof.make_thm 
     1.6    + ? how to do algebraic operations on numerals ? Presburger ? simplifier ?
     1.7 -  + clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
     1.8  
     1.9  * WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
    1.10        Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)