# HG changeset patch
# User wenzelm
# Date 911383202 -3600
# Node ID 669d0bc621e17cbe7cf853cdcd8a410d57f1baa7
# Parent  b9d5f5901b59c748c9eb4f1524f385765e5732d0
tuned comments;

diff -r b9d5f5901b59 -r 669d0bc621e1 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Nov 18 10:59:44 1998 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Nov 18 11:00:02 1998 +0100
@@ -5,8 +5,7 @@
 Derived theory operations.
 
 TODO:
-  - add_constdefs (atomic!);
-  - load theory;
+  - pure_thy.ML: add_constdefs (atomic!);
   - 'methods' section (proof macros, ML method defs) (!?);
   - next_block: ProofHistory open / close (!?);
 *)