blob: 81ebe3d5ba6cb71f26699c07bdda6d7bc0037849 (
plain)
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
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
---------------------------------------
* Code cleanups and improvements.
|
