Summary of Changes for Proof General 2.2 from 2.1
-------------------------------------------------

Generic Changes
---------------

* [XEmacs only]
  New function control-button1 (proof-mouse-track-insert) copies 
  individual commands (highlighted regions) from an open proof.  
  When a proof is closed, it behaves as mouse-track-insert
  (default XEmacs behaviour of control-button1).  
  

* New function C-c C-f (proof-find) to invoke some prover-specific
  mechanism to search for theories.  

* [XEmacs only] Toolbar has five new buttons (State, Context, Info, 
  Command, Help) which invoke commands previously available on keys/menus.
  Also a new "Find" button for proof-find.

* [XEmacs only] Toolbar enablers have been added.   
  Buttons are automatically enabled or disabled as appropriate.   
  This requires XEmacs 20.4 or better for reliable working.  
  

* Menus and keybindings have been reorganized.  
  Now keybindings invoke same functions as toolbar.

* Terminal string now automatically added to command for C-c C-v 

* Cleaned up example files so all demonstrate same theorem "conj_comms".
  Would be nice to add more theorems to compare scripts/proofs in
  different systems.  Please send in example scripts!

* Shorter buffer names for convenience.
 
* Removed transparent gif (text logo) from splash screen 
  because XEmacs can't display it nicely.
 
* Documentation updates.


Coq Changes
-----------

* Set proof-{qed,save}-commands so the toolbar functions work.


Isabelle and Isar Changes
-------------------------

* Tweaks for input syntax.  

* Recognize goals of the old form val prems = goal ...


Only in the developers' release
-------------------------------

* Provisional instantiation of Proof General for
  Plastic (http://www.dur.ac.uk/CARG/plastic.html)
  by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.


Internal changes for developers to note
---------------------------------------

* proof-shell-leave-annotations-in-output variable has been added.
  This allows quick and dirty mark up of output from the proof
  assistant using special characters with codes above 128 and
  font-lock.  Such characters are hidden from display in the
  output buffers.  
  However, it is NOT recommended to use this mechanism, because
  it breaks the usability of cut and paste (which copies the
  special characters).  Furthermore the entire mechanism of
  using special character codes is fragile and needs replacing
  in future versions of Proof General!

* Code cleanups and improvements.