1.1 --- a/TODO.md	Mon Jun 21 21:59:10 2021 +0200
     1.2 +++ b/TODO.md	Mon Jun 21 22:08:01 2021 +0200
     1.3 @@ -1,7 +1,3 @@
     1.4 -* reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
     1.5 -  + consider in Build_Thydata:  Thy_Hierarchy.insert_errpatIDs
     1.6 -  + consider in Biegelinie.thy: KEStore_Elems.add_thes, 
     1.7 -
     1.8  * MW: check uses of Unsynchronized.ref vs. Synchronized.var;
     1.9  
    1.10  * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
    1.11 @@ -15,10 +11,13 @@
    1.12      >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
    1.13  
    1.14  
    1.15 +* Eliminate Thy_Info.get_theory eventually: should take theory from ancestory
    1.16 +  within current context.
    1.17 +
    1.18  * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);
    1.19  
    1.20 -* Is it possible to eliminate union_overwrite, in favour of more standard data
    1.21 -  add/merge discipline?
    1.22 +* KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge?
    1.23 +  (Exception: rlss with its special cross-theory merge.)
    1.24  
    1.25  * What is the purpose of "#numeral" instead of plain numeral?
    1.26  
    1.27 @@ -38,6 +37,7 @@
    1.28      - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
    1.29  
    1.30  * WN: proper formal context with theory HOL-Library.Float, proper antiquotation @{const_name Float};
    1.31 +  (e.g. theory ISAC_Base imports "HOL-Library.Floar" instead of HOL.Complex_Main);
    1.32  
    1.33  * WN: clarify Rule.Thm ("minus_divide_left", ...): Should this be @{rule_thm_sym} antiquotation?
    1.34