1.1 --- a/TODO.md	Sat Aug 14 13:52:23 2021 +0200
     1.2 +++ b/TODO.md	Sat Aug 14 15:18:48 2021 +0200
     1.3 @@ -41,15 +41,7 @@
     1.4  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
     1.5    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
     1.6  
     1.7 -* WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
     1.8 -    ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close>
     1.9 -
    1.10 -* WN: Avoid Thm.get_name_hint --- somewhat fragile.
    1.11 -    Thm.get_name_hint supports lazyness of students, who do not care about theories
    1.12 -    a theorem is defined in.
    1.13 -    Dropping it, e.g. in "fun revert_sym_rule", breaks tests on Thy_Write.thydata,
    1.14 -    which shall be dropped; see e587c45cae0f note in Build_Thydata.thy.
    1.15 -  + what remains TODO: use Global_Theory.get_thm instead, get theory from References.T
    1.16 +* WN: Avoid Thm.get_name_hintand use Global_Theory.get_thm instead, get theory from References.T
    1.17      and push theory through as argument of respective functions.
    1.18  
    1.19  * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
    1.20 @@ -64,10 +56,6 @@
    1.21    + ? how do algebraic operations on numerals ? Presburger ? simplifier ? hack see
    1.22      https://hg.risc.uni-linz.ac.at/wneuper/isa/file/a14022b99b92/src/Tools/isac/ProgLang/evaluate.sml#l210
    1.23  
    1.24 -* WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
    1.25 -      Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
    1.26 -      Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
    1.27 -
    1.28  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
    1.29        ???
    1.30