1.1 --- a/TODO.md	Tue Aug 10 11:29:33 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 10 11:54:12 2021 +0200
     1.3 @@ -12,7 +12,8 @@
     1.4  
     1.5  
     1.6  * Eliminate Thy_Info.get_theory eventually: should take theory from ancestory
     1.7 -  within current context.
     1.8 +  within current context. cf. e587c45cae0f note in Build_Thydata.thy
     1.9 +    cf. e587c45cae0f note in Build_Thydata.thy
    1.10  
    1.11  * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);
    1.12  
    1.13 @@ -24,9 +25,10 @@
    1.14  * Check/clarify Context.theory_name vs. Context.theory_long_name.
    1.15  
    1.16  * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
    1.17 +    shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy
    1.18  
    1.19  * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
    1.20 -  
    1.21 +    cf. e587c45cae0f note in Build_Thydata.thy
    1.22  
    1.23  * WN: clarify add_calcs with non-existant constant "Integrate.add_new_c";
    1.24