1.1 --- a/TODO.md	Mon Jun 21 15:42:53 2021 +0200
     1.2 +++ b/TODO.md	Mon Jun 21 15:50:58 2021 +0200
     1.3 @@ -27,18 +27,21 @@
     1.4  * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
     1.5  
     1.6  
     1.7 +* WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
     1.8 +  e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
     1.9 +
    1.10  * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
    1.11      - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
    1.12  
    1.13 +* WN: proper formal context with theory HOL-Library.Float, proper antiquotation @{const_name Float};
    1.14 +
    1.15  * WN: clarify Rule.Thm ("minus_divide_left", ...): Should this be @{rule_thm_sym} antiquotation?
    1.16  
    1.17  * WN: check remaining MethodC.prep_input that use a different theory (e.g. "Diff"):
    1.18    Is this really required, or can we just use the 'method' command?
    1.19  
    1.20 -* WN: remove always empty arguments in MethodC.prep_input and Problem.prep_input
    1.21 -  (following the "TODO" comment);
    1.22 -
    1.23 -* WN: trim-down MethodC.prep_input and Problem.prep_input to what is really needed.
    1.24 +* WN: trim-down MethodC.prep_input and Problem.prep_input to what is really needed;
    1.25 +  improve errors via parse_term_strict;
    1.26  
    1.27  * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
    1.28