1.1 --- a/TODO.md	Mon Jun 21 21:53:23 2021 +0200
     1.2 +++ b/TODO.md	Mon Jun 21 21:59:10 2021 +0200
     1.3 @@ -26,6 +26,10 @@
     1.4  
     1.5  * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
     1.6  
     1.7 +* What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
     1.8 +
     1.9 +
    1.10 +* WN: clarify add_calcs with non-existant constant "Integrate.add_new_c";
    1.11  
    1.12  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
    1.13    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";