diff -r 0c10aeff57d7 -r e5e9a6c45597 TODO.md
--- a/TODO.md	Sat Jul 17 14:05:28 2021 +0200
+++ b/TODO.md	Sun Jul 18 16:20:32 2021 +0200
@@ -30,8 +30,10 @@
     - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
 
 * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation, DONE partially;
-    - TODO: ? how to do algebraic operations on numerals ? Presburger ? simplifier ?
-    - TODO: clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
+  + TOODOO are exclusive for this changeset; most follow from TOODOO.1
+  + TOODOO.1: exception TYPE raised by Skip_Proof.make_thm 
+  + ? how to do algebraic operations on numerals ? Presburger ? simplifier ?
+  + clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
 
 * WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
       Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)