1.1 --- a/TODO.md	Tue Apr 20 21:31:00 2021 +0200
     1.2 +++ b/TODO.md	Tue Apr 20 23:20:45 2021 +0200
     1.3 @@ -17,7 +17,11 @@
     1.4  * reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
     1.5  
     1.6  
     1.7 -* MW: check JVM resource requirements of session Isac_Test;
     1.8 +* MW: ML antiqutation @{rule_thm NAME} to produce (Rule.Thm ("NAME", ThmC.numerals_to_Free "NAME"));
     1.9 +
    1.10 +* MW: more concise "setup KEStore_Elems.add_rlss" etc.;
    1.11 +
    1.12 +* MW: eliminate low-level TextIO (not portable);
    1.13  
    1.14  * MW: check uses of Unsynchronized.ref vs. Synchronized.var;
    1.15  
    1.16 @@ -46,4 +50,14 @@
    1.17      - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
    1.18  
    1.19  * WN: investigate errors further which popped up in rewriting when replacing ^^^ by \<up> in ac7426ab0491.
    1.20 -      The errors occur with examples in test/../poly.sml, which do not work properly in isabisac20 either.
    1.21 \ No newline at end of file
    1.22 +      The errors occur with examples in test/../poly.sml, which do not work properly in isabisac20 either.
    1.23 +
    1.24 +* WN: cleanup remaining ^^^ in comments (but sometimes it is just ASCII art);
    1.25 +
    1.26 +* WN: simplify const names like "is'_expanded": no need to imitate the escape of mixfix syntax;
    1.27 +
    1.28 +* WN: proper statement for rcancel_den ("not" is a free variable!?!!):
    1.29 +    rcancel_den:             "not(a=0) ==> a * (b / a) = b" and
    1.30 +
    1.31 +* WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
    1.32 +