aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
blob: 242f7a3fa302e44b18f0be050a2278b9f6d6df0c (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
Summary of Changes for Proof General 2.1
----------------------------------------

* Two new provisional instantiations of Proof General, for:
   ** Isabelle/Isar (new proof language for Isabelle) by 
      Markus Wenzel <wenzelm@informatik.tu-muenchen.de>
   ** Plastic (http://www.dur.ac.uk/CARG/plastic.html)
      by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.

* Documentation improvements.   
  Information added for Coq mode.

* In proof-site.el, the environment variable PROOFGENERAL_ASSISTANTS 
  is examined for the default value of proof-assistants.  This
  means that no editing of proof-site.el should normally be 
  needed now. 

* Support for x-symbol package to beautify 
  input and output with special fonts.
  Patches for Isabelle provided by David von Oheimb.
  (currently incomplete)

* Improvements to Coq mode: better recognition of
  Coq syntax, support for proof-shell-restart-cmd.

* Bug fix for templates in Isabelle theory file mode.

* Bug fix for long-lines with funny characters causing
  ^G's in Solaris.

* Bug fix for case-insensitive matching.  Added 
  proof-case-fold-search configuration variable to
  allow for proof script languages with case-insensitive 
  syntax.

* Other minor bug fixes.