Changes for development release

1 files changed, 6 insertions, 144 deletions

diff --git a/CHANGES b/CHANGES
index ebece014..e9a47964 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,151 +1,13 @@
 -*- outline -*-
 
-* Summary of Changes for Proof General 3.4 from 3.3
+---   This is a development release of Proof General,     ---
+---   some features may be incomplete or buggy.  Please   ---
+---   report any problems to support@proofgeneral.org,    ---
+---   thanks.  Check files BUGS and <prover>/BUGS first.  ---
 
-** Generic Changes
 
-*** LICENSE CHANGE to GPL!
+* Summary of Changes for Proof General 3.5pre from 3.4
 
-It is now permitted to use Proof General in any context, without
-applying for a special license from University of Edinburgh.  
-Free redistribution is also allowed under the GPL conditions.
 
-*** Support added for GNU Emacs 21.X; no support for GNU Emacs 20.X
+ <<  No changes yet >>
 
-Toolbar, splash screen, and X-Symbol are all supported in GNU Emacs.  
-
-Sorry, this version of PG does not support Emacs 20; backwards
-compatibility is far too difficult to maintain.
-
-*** Colours altered
-
-Colours made a little less lurid.  Reverse video tweaks.
-(Look in proof-config for proof-locked-face, proof-queue-face
-and old settings if you want to change back: 
-use M-x customize-face, M-x list-faces-display, 
-M-x list-colours-display to play with your own defaults).
-
-*** Improvements to visibility controls
-
-Visibility controls now work for comments as well as proofs in
-proof scripts.  An image is used in XEmacs to signal hidden text.
-
-*** Context-sensitive menu (right mouse) now has additional features
-
-The context sensitive menu for regions of the buffer which have
-been processed allows several features, including hiding/revealing
-the area, copying it, and some prover-specific commands -- in
-Isabelle you can ask for a graph of the theorem dependencies (thm_deps),
-in Coq you can ask for the proof term to be printed.  
-(Please send us suggestions for other useful features here).
-
-*** Menu improvements (favourites, options saving)
-
-Favourites are now more robust.  You can delete them and save them
-when you want.  The PG "quick" options can also be saved separately
-from other Emacs custom variables.
-
-*** Support for "tracing" buffers improved and enabled by default.
-
-(Tracing is only deployed in Isabelle so far)
-Compared with experimental tracing in PG 3.3, there is now only one
-tracing buffer, treated somewhat like a response buffer.
-For minor issues, see isa/BUGS.
-
-*** Easily remove handling for provers you don't want 
-
-You can simply remove the directories from the PG distribution,
-instead of customizing the `proof-assistants' variable.
-
-*** Desktop integration for RedHat 7.3, Mandrake 8.2 in RPM package.
-
-RPM package now works on RedHat as well as Mandrake, and adds PG application
-to desktop menus.
-
-*** Efficiency improvements 
-
-Process buffers no longer keep undo information.
-
-
-
-** Isabelle Changes
-
-*** Isabelle/Isar syntax changes, other tweaks for Isabelle2002.
-
-Switch to using Isabelle/Isar by default for .thy files.
-Support next error function.
-
-Isabelle classic mode: highlighting tweaks for ML code contributed by
-Lucas Dixon (lucasd@dai.ed.ac.uk)
-
-*** Active highlighting of variables  [ EXPERIMENTAL FEATURE: see README.exper ]
-
-Variables are made active in the goals buffer.  Hovering the mouse
-over an identifier shows its type.  
-
-This handy feature is a glimpse of what could be done with proper
-subterm markup, which needs support to be added in the Isabelle core.
-
-
-** Coq Changes
-
-*** Much improved synchronization of PG/Coq. 
-
-Commands like Hint, Require, etc, were not backtracked correctly, but
-are now. Nested proofs and commands nested in proofs are now also well
-backtracked.
-
-User defined keywords could not completely well backtracked. The
-fall-back mechanism is better now, but to solve this completely we
-provide four configurable variables for registering personal tactics
-and commands. Commands and tactics are split into state-preserving or
-state-changing commands and tactics, i.e. which need or not Back/Undo
-to be backtracked. This allows PG to
-1) (more important) to correctly backtrack user-defined commands and
-   tactics.
-2) colorize correctly 
-
-See `coq-user-state-preserving-commands, `coq-user-state-changing-commands,
-`coq-user-state-preserving-tactics, `coq-user-state-changing-tactics'
-
-These variables are regexp lists. See their documentations in emacs of
-this variable (C-h v coq-user...) and in the doc, for details on how
-to set them in your .emacs file.  Example:
-
- An example of existing commands that fit each category:
-
-   coq-user-state-preserving-commands: example: "Print"
-
-   coq-user-state-changing-commands:     example: "Require"
-
-   coq-user-state-changing-tactics:      example: "Intro"
-
-   coq-user-state-preserving-tactics:  example: "Proof"
-
-   This variables are string lists. See the documentations in emacs of
-   this variable (C-h v coq-user...)  for details on how to set them
-   in your .emacs file.
-
-   Example:
-   (setq coq-user-state-changing-commands 
-	  '("MyHint" "MyRequire" "Show\\-+Mydata"))
-
-	Last thing: you must restart emacs to allow emacs take these
-	variable into account.
-
-
-** Changes for other provers
-
-*** ACL2 improved (now issues undo commands)
-Still experimental and in need of official support.
-
-
-** Changes for proof assistant developers to note
-  
-*** Improvements in instantiation mechanism
-
-Allow smoother support for provers which only use scripting, and do
-not make use of goals window (e.g. Twelf, ACL2).  We no longer warn if
-inessential settings like proof-goal-command and similar are unset,
-but instead automatically remove toolbar and menu items
-correspondingly.