1.1 --- a/TODO.md	Tue Aug 10 11:01:18 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 10 11:29:33 2021 +0200
     1.3 @@ -26,29 +26,17 @@
     1.4  * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
     1.5  
     1.6  * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
     1.7 -
     1.8 +  
     1.9  
    1.10  * WN: clarify add_calcs with non-existant constant "Integrate.add_new_c";
    1.11  
    1.12  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
    1.13    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
    1.14  
    1.15 -* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
    1.16 -    - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
    1.17 -
    1.18 -* WN: proper formal context with theory HOL-Library.Float, proper antiquotation @{const_name Float};
    1.19 -  (e.g. theory ISAC_Base imports "HOL-Library.Floar" instead of HOL.Complex_Main);
    1.20 -
    1.21 -* WN: clarify Rule.Thm ("minus_divide_left", ...): Should this be @{rule_thm_sym} antiquotation?
    1.22 -
    1.23  * WN: check remaining MethodC.prep_input that use a different theory (e.g. "Diff"):
    1.24    Is this really required, or can we just use the 'method' command?
    1.25  
    1.26 -* WN: trim-down MethodC.prep_input and Problem.prep_input to what is really needed;
    1.27 -  improve errors via parse_term_strict;
    1.28 -
    1.29  * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
    1.30 -
    1.31      ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close>
    1.32  
    1.33  * WN: Avoid Thm.get_name_hint --- somewhat fragile.