From 49b87a2ce35e79f362d998f05cd09b4f8fc07441 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 9 May 2000 15:58:46 +0000
Subject: Note about desirable additions to Isabelle

---
 isa/todo | 6 ++++++
 1 file changed, 6 insertions(+)

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?
-- 
cgit v1.2.3