diff options
| -rw-r--r-- | BUGS | 2 | ||||
| -rw-r--r-- | etc/announce | 21 | ||||
| -rw-r--r-- | todo | 10 |
3 files changed, 18 insertions, 15 deletions
@@ -2,7 +2,7 @@ * Known Bugs and Workarounds for Proof General. -Contact: mailto:proofgen@dcs.ed.ac.uk +Contact: mailto:bugs@proofgeneral.org See also: http://www.proofgeneral.org/ProofGeneral/BUGS Generic bugs are listed here, which may affect all of the supported diff --git a/etc/announce b/etc/announce index ca5726fb..58276c65 100644 --- a/etc/announce +++ b/etc/announce @@ -32,22 +32,15 @@ tag for comp.lang.ml, comp.lang.functional: Subject: Proof General --- Version 3.2 release -[Apologies for multiple copies] - - Announcing Proof General Version 3.2 - - A Generic Emacs interface for Interactive Proof Assistants - + A Generic Emacs interface for Interactive Proof Assistants http://www.proofgeneral.org - contact: David Aspinall <da@dcs.ed.ac.uk> - - ========================= + contact: David Aspinall <da@proofgeneral.org> -Proof General is an (X)Emacs interface for developing proof scripts. +Proof General is a generic (X)Emacs interface for proof assistants. It can be instantiated for the proof assistant of your choice, and is -supplied ready-customised for Isabelle, Coq, LEGO, and HOL. +supplied ready-customised for Isabelle, Coq, LEGO, HOL, and AF2. Proof General includes these features, amongst others: @@ -76,9 +69,9 @@ The user manual contains full details, and is available on-line at: http://www.proofgeneral.org/index.phtml?page=doc Proof General needs a recent version of Emacs to run with, and it much -prefers XEmacs to FSF GNU Emacs. Proof General 3.1 has been tested -with XEmacs 21.1 and Emacs 20.5. (It should work back to XEmacs 20.4 -and Emacs 20.2, though). +prefers XEmacs to FSF GNU Emacs. Proof General 3.2 has been tested +with XEmacs 21.1 and Emacs 20.7. (It may work back to XEmacs 20.4 and +Emacs 20.2, though). Installing Proof General is easy. Why not give it a try? @@ -36,6 +36,16 @@ B Keybindings for processing theory in thy mode gone?? ** 2. Things to in the generic interface +*** B Move 3.3 over to new better designed parsing function mechanism. + +*** D some renaming for uniformity: + + proof-comment-start -> proof-script-comment-start, ditto end + +*** B Generalize electric terminator mode for other parsing mechanisms. + +*** B Add parameter for help function so HOL help works nicely + *** B Make tags support in lego.el and coq.el a bit more generic. Use customization option proof-tags-support. |