diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-13 13:11:36 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-13 13:11:36 +0000 |
| commit | 9f5a0a3814b00df9c7c393831db986ae18f8704b (patch) | |
| tree | 895bc2c0c271d696fc1fb6517390308527177de8 /TODO | |
| parent | a8a5c264a995cf1bd4f15d34ee6cdc03f4ff7e94 (diff) | |
Mention plans to implement PGIP support.
Diffstat (limited to 'TODO')
| -rw-r--r-- | TODO | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -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. |