From 9f5a0a3814b00df9c7c393831db986ae18f8704b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 13 Apr 2004 13:11:36 +0000
Subject: Mention plans to implement PGIP support.

---
 TODO | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/TODO b/TODO
index 1385396e..3390f8d6 100644
--- a/TODO
+++ b/TODO
@@ -14,9 +14,12 @@ da+pg-feedback@inf.ed.ac.uk.  Thanks!
 Plans for upcoming versions
 ---------------------------
 
+* Implement support for PG Kit.  Support PGIP provers fully, with/without 
+  mediator.   (See http://proofgeneral.inf.ed.ac.uk/kit).
+
 * Use CEDET Emacs framework for development tools, to allow more
   powerful parsing of proof scripts and features arising from that.  
-  See http://cedet.sourceforge.net/.
+  (See http://cedet.sourceforge.net/).
 
 * Add a browser mode for browsing script files and/or live theory
   data-structures, in the prover.
@@ -24,9 +27,6 @@ Plans for upcoming versions
 * More flexible goals buffer mode to allow menus of common proof
   commands, especially via PBP-style highlighting
 
-* Implement ideas in the Proof General White Paper. 
-  (See the Development section of the web page for a link).
-
 * Queue manipulation improvement: allow to extend or reduce
   during processing, with fewer "Proof Process Busy" messages.  
 
-- 
cgit v1.2.3