blob: 984f7ab478cacbb4a94cdd24d72298aa238de064 (
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
|
-*- outline -*-
* Summary of Changes for Proof General 3.2 from 3.1
** Generic Changes
*** Added proof assistant specific menu facility.
Specific menus added for Coq, Isabelle.
*** Proof assistant specific keymap added
Keybindings for proof assistant now begin with "C-c a".
*** Improved behaviour of electric terminator
*** Efficiency improvement in parsing
Also works around crash bug in xemacs-21.1.7/SuSE.
Fix by Markus Wenzel.
*** Added possibility for switching prover's output on/off.
Already implemented in Coq and Isabelle(/Isar).
** Coq Changes
*** More decoration of Coq output, uses CoqResp mode now
** LEGO Changes
*** Slight change in output during proof: shows final discharge messages
This is a side effect of code rationalization in PG elsewhere.
** Isabelle Changes
*** Fix for stack overflow in regexp which occurred with large proof states
** Isar Changes
** HOL Changes
*** Output decoration improvements.
** Changes for developers to note
*** No need for match string 1 in proof-shell-proof-completed
*** Changed buffer mode name: pbp-mode -> proof-goals-mode, for uniformity.
|
