blob: 5d5fc3c8456e8ac1cddc1c52c48e208618bdbd3f (
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
|
Summary of Changes for Proof General 3.1 from 3.0
=================================================
Generic Changes
---------------
Fixes for supporting Japan versions of Emacs which have older CL macs
with Japanicised documentation. (Japan users, please report any other
problems you find, they may be fixable for similar reasons).
Minor bug fix for duplicated short output.
(set proof-shell-eager-annotation-start-length appropriately)
Bug fix with .thy files and X-Symbol mode: subsequently visited
theory files would have X-Symbols broken.
Bug fix for (non-mule) FSF Emacs 20.5. (Emacs would freeze when
starting proof assistant due to character matching problem).
Fix for infamous Solaris ^G problem, by setting
process-connection-type=nil to force piped communication instead of
ptys. (This may have other side effects so please report any you
suspect).
Coq Changes
-----------
LEGO Changes
------------
Isabelle Changes
----------------
Isar Changes
------------
Minor syntax tweaks.
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
---------------------------------------
No changes.
|
