1.1 --- a/TODO.md	Wed Aug 11 11:54:07 2021 +0200
     1.2 +++ b/TODO.md	Sat Aug 14 13:52:23 2021 +0200
     1.3 @@ -45,6 +45,12 @@
     1.4      ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close>
     1.5  
     1.6  * WN: Avoid Thm.get_name_hint --- somewhat fragile.
     1.7 +    Thm.get_name_hint supports lazyness of students, who do not care about theories
     1.8 +    a theorem is defined in.
     1.9 +    Dropping it, e.g. in "fun revert_sym_rule", breaks tests on Thy_Write.thydata,
    1.10 +    which shall be dropped; see e587c45cae0f note in Build_Thydata.thy.
    1.11 +  + what remains TODO: use Global_Theory.get_thm instead, get theory from References.T
    1.12 +    and push theory through as argument of respective functions.
    1.13  
    1.14  * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
    1.15      - quite often "axiomatization ..." can be turned into "lemma ... by auto"
    1.16 @@ -71,4 +77,4 @@
    1.17  
    1.18  * WN: push suggestions of MW through the whole code
    1.19    + e1da148725ed : \<^ML>\<open>...\<close> instead of parentheses
    1.20 -  + 
    1.21 \ No newline at end of file
    1.22 +  +