From 9696feae2f1cab56a375a8881a3a9483fd5eb3c7 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 19 Feb 2003 12:13:07 +0000
Subject: Updated.

---
 isar/todo | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'isar')

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
-- 
cgit v1.2.3