command 'thm' makes no sense outside a proper context;

fixed spelling;

1 files changed, 1 insertions, 7 deletions

diff --git a/isar/todo b/isar/todo
index 75da5f95..cfb5578e 100644
--- a/isar/todo
+++ b/isar/todo
@@ -24,12 +24,6 @@ See also ../todo for generic things to do, priority codes.
 
 ** C Electric terminator for non-terminator provers would be nice.
 
-** 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 Proof nesting depth calculation not right: see debug messages
 
 ** B Isabelle tweaks
@@ -46,4 +40,4 @@ See also ../todo for generic things to do, priority codes.
 
 ** C provide template for empty theory (or even just for Scratch.thy);
 
-** C proper proof-by-pointing support (vary hard);
+** C proper proof-by-pointing support (very hard);