CHANGES


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

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

* Toolbar has four new buttons: Show, Context, Info, Command
  These invoke commands previously available on keys/menus.

* Toolbar enablers have been added.   
  Buttons are automatically enabled or disabled as appropriate.   
  This may require XEmacs 21 for reliable working.  
  (Toolbar only works with XEmacs)

* Tweaks for Isabelle and Isar syntax.  Fixed problem with
  recognizing goals of the old form val prems = goal ...

* 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!

* Other minor improvements and alterations:
  - Shorter buffer names (esp for Coq).
  - Set proof-{qed,save}-commands so the toolbar functions work.
  - Removed transparent gif from splash screen because XEmacs can't
    display it nicely.
  - Documentation updates


Only in the developer's 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>.