1 files changed, 6 insertions, 0 deletions
diff --git a/isar/todo b/isar/todo
index 3b76d39a..0adc6508 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,6 +4,12 @@
 
 See also ../todo for generic things to do, priority codes.
 
+** B theorem dependencies: using Isar's "thm" command does not
+   work at top level.  This is annoying for browsing the fully
+   qualified dependency names.  (Even the ML_command "thm"
+   returns unknown theory context error).  Can we use something
+   else?
+
 ** B visualise dependencies: sometimes not applicable.
 
 ** C func-menu: observe proof-syntactic-context (general problem of