From a8e9cd2171bc46aa199eefbbb7de2dee390b4118 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Tue, 13 Nov 2007 16:17:01 +0000
Subject: command 'thm' makes no sense outside a proper context; fixed
 spelling;

---
 isar/todo | 8 +-------
 1 file changed, 1 insertion(+), 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);
-- 
cgit v1.2.3