# 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 (!?); *)