1.1 --- a/TODO.md	Tue Aug 10 19:05:59 2021 +0200
     1.2 +++ b/TODO.md	Wed Aug 11 11:54:07 2021 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4      cf. e587c45cae0f note in Build_Thydata.thy
     1.5  
     1.6  * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);
     1.7 +    ??
     1.8  
     1.9  * KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge?
    1.10    (Exception: rlss with its special cross-theory merge.)
    1.11 @@ -24,6 +25,9 @@
    1.12      ??
    1.13  
    1.14  * Check/clarify Context.theory_name vs. Context.theory_long_name.
    1.15 +    present ISAC assumes 2 sessions in the MathEngine, Specify and Interpret, 
    1.16 +    and all Isac_Knowledge is in session Isac.
    1.17 +    So Context.theory_name suffices
    1.18  
    1.19  * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
    1.20      shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy