Updated for 3.1, removed appendix.

1 files changed, 14 insertions, 87 deletions

diff --git a/etc/announce b/etc/announce
index 989f1728..5ec20069 100644
--- a/etc/announce
+++ b/etc/announce
@@ -35,12 +35,12 @@ tag for comp.lang.ml, comp.lang.functional:
 
  
         
-Subject: Proof General --- Version 3.0 release
+Subject: Proof General --- Version 3.1 release
 
 [Apologies for multiple copies]
 
 
-            Announcing  Proof General  Version 3.0
+            Announcing  Proof General  Version 3.1
 
    A Generic Emacs interface for Interactive Proof Assistants
 
@@ -52,7 +52,7 @@ Subject: Proof General --- Version 3.0 release
 
 Proof General is an Emacs interface for developing proof scripts.
 It can be instantiated for the proof assistant of your choice,
-and is supplied ready-customised for Isabelle, Coq, and LEGO.
+and is supplied ready-customised for Isabelle, Coq, LEGO, and HOL.
 
 Proof General includes these features, amongst others:
 
@@ -65,99 +65,26 @@ Proof General includes these features, amongst others:
 . Provision to easily run proof assistant on a remote host
 . Works on any platform Emacs does, in window system or plain console 
 
-Summary of changes since 2.1:
+Summary of changes since 3.0:
 
-. Eight new toolbar buttons, now enabled depending on context
-. Improved and reorganized menus and key-bindings, options settings
-. Much easier to adapt to new systems, comes with example (< 30 setqs)
-. New function to search for theorems 
-. X-Symbol support for Coq, LEGO, and Isabelle
-. Lots more fine-grained improvements, for full details
-  http://www.lfcs.informatics.ed.ac.uk/proofgen/ProofGeneral-3.0/CHANGES
+. New instantiation for HOL98!  Test release.
+. Minor cosmetic improvements 
+. Bug fixes for Emacs compatibility (FSF, Japanese versions, XEmacs on win32)
+. Fix for infamous Solaris ^G bug
+. Several other bug fixes
+. For full details, see
+  http://www.lfcs.informatics.ed.ac.uk/proofgen/ProofGeneral-3.1/CHANGES
 
 The user manual contains full details, and is available on-line at: 
 http://www.lfcs.informatics.ed.ac.uk/proofgen/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.0 has been tested
-with XEmacs 21.1 and Emacs 20.4.  (It should work back to XEmacs 20.4
+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).  
 
 Installing Proof General is easy.  Why not give it a try?
 
  - David Aspinall <da@dcs.ed.ac.uk>
-
-
-
-
-Appendix
-========
-
-
-
-The rest of this announcement contains notes addressed to different
-user communities: LEGO, Coq, and Isabelle; users of other proof
-assistants, user-interface/theorem-proving researchers and, finally,
-Emacs gurus.
-
-
-To users of LEGO, Coq, and Isabelle:
-------------------------------------
-
-Proof General 3.0 has several new features as well as bug fixes and
-improvements over versions 2.1 and 2.0.  It supports the latest
-theorem prover versions: LEGO 1.3.1, Coq 6.3 and Isabelle 99.
-
-Please try it and let us know what you think of it!
-
-We have worked hard on the user documentation, and on making Proof
-General robust and easy to install.
-
-
-To users of other proof assistants:
------------------------------------
-Our aim is provide a powerful and configurable Emacs mode which helps
-user-interaction with interactive proof assistants.
-
-Please help us with this aim!  The code of Proof General is designed
-to be adaptable to other proof assistants, by writing a little bit of
-Emacs Lisp (mainly regular expressions).  If you are using or
-designing another proof assistant, please try configuring Proof
-General for it, and let us know how you get on.
-
-
-To user-interface/theorem-proving researchers:
----------------------------------------------- 
-Proof General provides a unified interface to different theorem
-provers.  The advantage is that a novice who understands the Proof
-General interface can inspect and replay proofs in any of the theorem
-provers supported, without knowing the specific commands needed to
-drive them.  Moreover, by implementing your user-interface ideas in
-the Proof General framework, your contributions automatically reach a
-large community of both novice and expert proof assistant users.
-
-A desirable avenue towards further and easier unification would be to
-invent a unified proof script (input) language and proof-state
-(output) language for theorem provers. The Proof General experience
-could provide useful insight into such a project.  I'd be keen to hear
-from workers interested in collaborating in this area.
-
-
-To Emacs gurus: 
---------------- 
-If you happen to be an Emacs guru also interested in interactive
-proof, we want you to contribute to the development of Proof General!
-Please join in!  There are plenty of exciting avenues for improving
-this tool, for example, to add proof by pointing facilities (a basis
-already exists for LEGO), and a theory browser.
-
-Apart from proof assistants, script management makes sense for many
-other systems or languages with an interactive shell-like interpreter.
-I would be keen to hear from any Emacs developers interesting in
-adapting Proof General's script management for development in Lisp,
-SML, or other languages.
-
-
- -- David Aspinall <da@dcs.ed.ac.uk>
-    December 1999.
+   March 2000.