aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2001-07-09 15:45:57 +0000
committerDavid Aspinall2001-07-09 15:45:57 +0000
commit4fde55ed2601e61a4a490073a38bbbec6b124b1e (patch)
treef5584e987261c5b625a785048c4cd79668feb9c5
parent5d995f282d065c02dab95145eba4905a646d1ebc (diff)
TODO for proof-ass fixing added.
-rw-r--r--todo4
1 files changed, 4 insertions, 0 deletions
diff --git a/todo b/todo
index 2a8a62f3..bc3f6bca 100644
--- a/todo
+++ b/todo
@@ -32,6 +32,10 @@ X (Low) e.g. probably not worth spending time on
** 2. Things to in the generic interface
+*** C Fix byte compilation
+ Problem with proof-ass macro mechanism -- gets expanded during
+ compilation.
+
*** C The PG isabelle-completion-table seems to be subject to case-fold, which
it shouldn't be: \<sqinter> does not work, but \<Sqinter> is OK.