# HG changeset patch
# User wneuper <walther.neuper@jku.at>
# Date 1628589252 -7200
# Node ID de670839362e8b6907d4c58a7bf8095c5d3c7dc0
# Parent  e587c45cae0f18a56ee54ff3dbe8b2f9a6f71023
relate note on planned improvements (cf.03dea0a179d0) to TODO.md

diff -r e587c45cae0f -r de670839362e TODO.md
--- a/TODO.md	Tue Aug 10 11:29:33 2021 +0200
+++ b/TODO.md	Tue Aug 10 11:54:12 2021 +0200
@@ -12,7 +12,8 @@
 
 
 * Eliminate Thy_Info.get_theory eventually: should take theory from ancestory
-  within current context.
+  within current context. cf. e587c45cae0f note in Build_Thydata.thy
+    cf. e587c45cae0f note in Build_Thydata.thy
 
 * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);
 
@@ -24,9 +25,10 @@
 * Check/clarify Context.theory_name vs. Context.theory_long_name.
 
 * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
+    shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy
 
 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
-  
+    cf. e587c45cae0f note in Build_Thydata.thy
 
 * WN: clarify add_calcs with non-existant constant "Integrate.add_new_c";