1.1 --- a/TODO.md	Tue Jun 15 22:24:20 2021 +0200
     1.2 +++ b/TODO.md	Wed Jun 16 12:56:09 2021 +0200
     1.3 @@ -27,22 +27,28 @@
     1.4  * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
     1.5  
     1.6  
     1.7 -* WN: Avoid Thm.get_name_hint --- somewhat fragile.
     1.8 +* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
     1.9 +    - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
    1.10  
    1.11  * WN: clarify Rule.Thm ("minus_divide_left", ...): Should this be @{rule_thm_sym} antiquotation?
    1.12  
    1.13 +* WN: check remaining MethodC.prep_input that use a different theory (e.g. "Diff"):
    1.14 +  Is this really required, or can we just use the 'method' command?
    1.15 +
    1.16  * WN: remove always empty arguments in MethodC.prep_input and Problem.prep_input
    1.17    (following the "TODO" comment);
    1.18  
    1.19  * WN: trim-down MethodC.prep_input and Problem.prep_input to what is really needed.
    1.20  
    1.21 +* WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
    1.22 +
    1.23 +    ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close>
    1.24 +
    1.25 +* WN: Avoid Thm.get_name_hint --- somewhat fragile.
    1.26 +
    1.27  * WN: eliminate ThyC.to_ctxt, use Proof_Context.init_global inline to make more
    1.28    clear where the normal Isabelle context-discipline is bypassed;
    1.29  
    1.30 -* WN: standardize theory for KEStore_Elems.add_rlss, KEStore_Elems.add_mets, KEStore_Elems.add_pbts
    1.31 -    - should be always the current @{theory} of the enclosing "setup" command;
    1.32 -    - avoid old-style "val thy = @{theory}" somewhere in a theory file;
    1.33 -
    1.34  * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
    1.35      - quite often "axiomatization ..." can be turned into "lemma ... by auto"
    1.36        without further ado;
    1.37 @@ -50,17 +56,4 @@
    1.38      - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
    1.39      - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
    1.40  
    1.41 -* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
    1.42 -    - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
    1.43 -
    1.44 -* WN: Part.DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art);
    1.45 -      Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
    1.46 -      Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
    1.47 -
    1.48  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
    1.49 -
    1.50 -* WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
    1.51 -
    1.52 -ML \<open>
    1.53 -  val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
    1.54 -\<close>