diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-01-03 15:05:27 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-01-03 15:05:27 +0000 |
| commit | 8f60e0987c671e25f4ddd11e611acb82c7799ebe (patch) | |
| tree | b9bd6ab315d420746f73213c797520a8a90a0e14 /doc | |
| parent | 262519dc6039cb23aa21b36daaa5e76c38d0b76a (diff) | |
Add News for Version 4.2
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index daa90e5d..f7715aaf 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -199,14 +199,28 @@ other documentation, system downloads, etc. @menu +* News for Version 4.2:: * News for Version 4.1:: * News for Version 4.0:: * Future:: * Credits:: @end menu +@node News for Version 4.2 +@unnumberedsec News for Version 4.2 +@cindex news + +Proof General version 4.2 adds the usual round of compatibility fixes, +to support newer versions of Emacs and Coq. It also contains some +updates to support HOL Light in a primitive fashion. + +It also contains a new mechanism to display proof trees, provided by +Hendrik Tews and using a bespoke rendering application named +@uref{http://askra.de/software/prooftree/, Prooftree}. + + @node News for Version 4.1 -@unnumberedsec News for Version 4.0 +@unnumberedsec News for Version 4.1 @cindex news Proof General version 4.1 adds some compatibility fixes to @@ -471,6 +485,7 @@ script file for your proof assistant, for example: @item Isabelle @tab @file{.thy} @tab @code{isar-mode} @item Phox @tab @file{.phx} @tab @code{phox-mode} @item HOL98 @tab @file{.sml} @tab @code{hol98-mode} +@item HOL Light @tab @file{.ml} @tab @code{hol-light-mode} @item ACL2 @tab @file{.acl2} @tab @code{acl2-mode} @item Twelf @tab @file{.elf} @tab @code{twelf-mode} @item Plastic @tab @file{.lf} @tab @code{plastic-mode} |