1.1 --- a/TODO.md Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/TODO.md Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -63,4 +63,18 @@
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 + + clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
1.12 +
1.13 +* WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
1.14 + Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
1.15 + Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
1.16 +
1.17 * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
1.18 + ???
1.19 +
1.20 +* WN: reduce the number of TermC.parse*;
1.21 + - one or two variants should suffice.