Note about desirable additions to Isabelle

1 files changed, 6 insertions, 0 deletions

diff --git a/isa/todo b/isa/todo
index 405b209b..ec03621d 100644
--- a/isa/todo
+++ b/isa/todo
@@ -4,6 +4,12 @@
 
 See also ../todo for generic things to do, priority codes.
 
+** C Improvements to Isabelle that would be nice for Proof General:
+
+   -- ability to remove theorem from theorem database, issued
+   when undoing qed
+
+
 ** C Investigate fix for looping rewriting in Isabelle.  Continual
   and frequent messages from the prover lock out the user.
   Is there any easy way of fixing this?