1.1 --- a/TODO.md	Tue Aug 10 11:54:12 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 10 11:55:24 2021 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  
     1.6  * Eliminate Thy_Info.get_theory eventually: should take theory from ancestory
     1.7 -  within current context. cf. e587c45cae0f note in Build_Thydata.thy
     1.8 +  within current context.
     1.9      cf. e587c45cae0f note in Build_Thydata.thy
    1.10  
    1.11  * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);