1.1 --- a/TODO.md	Sat Aug 14 18:49:36 2021 +0200
     1.2 +++ b/TODO.md	Sat Aug 14 18:59:30 2021 +0200
     1.3 @@ -20,6 +20,9 @@
     1.4  
     1.5  * KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge?
     1.6    (Exception: rlss with its special cross-theory merge.)
     1.7 +    ? how adapt the different signatures ?
     1.8 +    union_overwrite: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
     1.9 +    merge          : ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.10  
    1.11  * What is the purpose of "#numeral" instead of plain numeral?
    1.12      ??
    1.13 @@ -41,7 +44,7 @@
    1.14  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
    1.15    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
    1.16  
    1.17 -* WN: Avoid Thm.get_name_hintand use Global_Theory.get_thm instead, get theory from References.T
    1.18 +* WN: Avoid Thm.get_name_hint and use Global_Theory.get_thm instead, get theory from References.T
    1.19      and push theory through as argument of respective functions.
    1.20  
    1.21  * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations