Deleted file

1 files changed, 0 insertions, 56 deletions

diff --git a/etc/announce b/etc/announce
deleted file mode 100644
index 45537576..00000000
--- a/etc/announce
+++ /dev/null
@@ -1,56 +0,0 @@
-            Announcing  Proof General  Version 3.6
-    A Generic Emacs interface for Interactive Proof Assistants
-              http://proofgeneral.inf.ed.ac.uk
-
-      Contact: David Aspinall <da+pg-feedback@inf.ed.ac.uk>
-
-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 PhoX, and, 
-experimentally, several other systems.
-
-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; hiding proofs
-. Display of real logical symbols, greek letters, etc with X-Symbol
-. Activation of prover output for subterm navigation, proof-by-pointing
-. Simplified communication: proof assistant verbosity hidden
-. Menus for jumping to theorems/definitions, etc 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 interesting changes since 3.5 (April 2004):
-
-. Updates and bug fixes for Coq 8.0
-. Extensions for development version of Isabelle, esp. PGIP support
-
-Summary of interesting changes since 3.4 (August 2002):
-
-. Speedbar and Index Menu.  Speedbar provides a handy file/tag tree.
-. Improved display management.  
-. RPM packages with freedesktop.org integration and compiled files
-. Keyboard hints and other messages displayed in minibuffer
-. Improved menus, user options, script colouring and active highlighting
-. For Coq (8.0): "holes" for editing expressions, extra menus, auto compilation
-. For Isabelle (2004): browsing/highlighting theorem dependencies
-. For Isabelle: using LaTeX mode for LaTeX parts of proof documents (via MMM)
-. New instances of PG: Casl Consistency Checker, Shell Script
-. Additional sample proofs (some from http://www.cs.kun.nl/~freek/comparison/)
-. Many other minor improvements and editing features
-. Many changes for compatibility with latest Emacsen (esp. GNU) and provers
-. Auxiliary modes bundled: X-Symbol and MMM (Multiple Major Mode)
-
-For details of changes since 3.4, see
-http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=ProofGeneral-3.6%2FCHANGES
-
-For the latest user manual, see http://proofgeneral.inf.ed.ac.uk/doc
-
-Proof General needs a recent version of Emacs to run with.  
-Proof General 3.6 has been tested with XEmacs 21.4.15, and 
-GNU Emacs 21.3.1.  Other recent versions of either Emacs may work but 
-are not guaranteed.
-
- - David Aspinall.
-   September 2004.