Update for 3.3

1 files changed, 18 insertions, 20 deletions

diff --git a/etc/announce b/etc/announce
index f43f9ec2..1dbda9ff 100644
--- a/etc/announce
+++ b/etc/announce
@@ -30,51 +30,49 @@ tag for comp.lang.ml, comp.lang.functional:
 
  
         
-Subject: Proof General --- Version 3.2 release
+Subject: Proof General --- Version 3.3 release
 
-            Announcing  Proof General  Version 3.2
+            Announcing  Proof General  Version 3.3
     A Generic Emacs interface for Interactive Proof Assistants
                  http://www.proofgeneral.org
 
-          contact: David Aspinall <da@proofgeneral.org>
+         contact: David Aspinall <da@proofgeneral.org>
 
 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, HOL, and AF2.
+supplied ready-customised for Isabelle, Coq, LEGO, and PhoX, and, 
+experimentally, for HOL, Twelf, and ACL2.
 
 Proof General includes these features, amongst others:
 
 . Script management: proof assistant state reflected in editor
 . Toolbar and menus: commands for building and replaying proofs
-. Syntax highlighting of proof scripts and prover output
+. Syntax highlighting of proof scripts and prover output; hiding proofs
 . Display of real logical symbols, greek letters, etc
 . Simplified communication: proof assistant verbosity hidden
 . Menu for jumping to theorems in a proof script
 . 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 3.1:
+Summary of changes since 3.2:
 
-. New provers: AF2 (full support) Twelf, ACL2 (experimental support) 
-. Integrated support for Isabelle upgraded for Isabelle99-1 
-. Each proof assistant now has its own menu with specific functions
-. Documentation is now split into user manual and "adapting" manual
-. Improvements in window management
-. New commands, including parsing of error messages 
-. Efficiency improvements
-. Several bug fixes 
-. Internal improvements: more flexible parsing and easier configuration
+. Visibility control for completed proofs
+. Dependency browsing/highlighting (currently Isabelle only)
+. Bug fixes 
+. Compatibility improvements: XEmacs 21.4, Coq 7, Windows
 
-The user manual contains full details, and is available on-line at: 
-http://www.proofgeneral.org/index.html?page=doc
+For details of changes since 3.2, see
+http://www.proofgeneral.org/fileshow.php?file=ProofGeneral-3.3%2FCHANGES
+
+For the latest user manual, see http://www.proofgeneral.org/doc
 
 Proof General needs a recent version of Emacs to run with, and it much
-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
+prefers XEmacs to FSF GNU Emacs.  Proof General 3.3 has been tested
+with XEmacs 21.4 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?
 
  - David Aspinall <da@dcs.ed.ac.uk>
-   October 2000.
+   September 2001.