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