diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-10-01 11:48:38 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-10-01 11:48:38 +0000 |
| commit | 7af0b5b970aa72c7b9997a8107c961ee99fce3ec (patch) | |
| tree | ecdf66343372c030cc32ed364da5135f9712c377 | |
| parent | 232d0543bbd73d719049bdd3f4184ba617f0506f (diff) | |
Update version numbers, release dates
| -rw-r--r-- | README | 15 | ||||
| -rw-r--r-- | coq/README | 8 | ||||
| -rw-r--r-- | isar/README | 2 |
3 files changed, 11 insertions, 14 deletions
@@ -6,9 +6,9 @@ environment for using interactive proof assistants. This is version 4.0 of Proof General. See About for exact version. -It is built for Emacs 23. The code should also work with Emacs 22.3, +It is built for Emacs 23. The code *may* also work with Emacs 22.3, but you will need to regenerated the byte-compiled files with "make -clean; make compile". +clean; make compile". Backward compatibility cannot be guaranteed. See INSTALL for installation details. @@ -25,15 +25,16 @@ Links: Wiki: http://proofgeneral.inf.ed.ac.uk/wiki Lists: http://proofgeneral.inf.ed.ac.uk/mailinglist -Supported proof assistants: Coq, Isabelle, LEGO, PhoX, Plastic -Experimental (less useful): CCC,ACL2,HOL98,Lambda-Clam,Shell,Twelf,Demoisa +Supported proof assistants: Coq, Isabelle, LEGO, PhoX +Experimental (less useful): CCC,ACL2,HOL98,Hol-Light,Lambda-Clam,Shell,Twelf + Obsolete instances: Demoisa,Lambda-Clam,Plastic A few example proofs are included in each prover subdirectory. The "root2" proofs of the irrationality of the square root of 2 were proofs written for Freek Wiedijk's challenge in his comparison of different theorem provers, see http://www.cs.kun.nl/~freek/comparison/. -Those proof scripts are copyright by their named authors. (NB: most -of these may have rusted) +Those proof scripts are copyright by their named authors. +(NB: most of these have rusted) Check BUGS files for some static problems and issues. Please report new bugs on the Trac site at http://proofgeneral.inf.ed.ac.uk/trac. @@ -42,4 +43,4 @@ For the latest news and downloads, visit Proof General on the web at: http://proofgeneral.inf.ed.ac.uk David Aspinall <da+pg-feedback@inf.ed.ac.uk> -September 2010. +October 2010. @@ -6,20 +6,16 @@ Later contributions by Patrick Loiseleur, Pierre Courtieu, Status: supported Maintainer: Pierre Courtieu -Coq version: 8.1 +Coq version: 8.2 Coq homepage: http://coq.inria.fr/ =========================================================================== Coq Proof General has support for Unicode Tokens, using simple character -sequences rather than a special language of tokens (which works well -with V8's new syntax!). See notes below. +sequences rather than a special language of tokens. See notes below. There is a tags program, coqtags. -There is a menu option for running Coq V8 in compatibility mode -(i.e. with the -translate flag), see Coq -> Settings. - =========================================================================== Installation notes: diff --git a/isar/README b/isar/README index 944f7a3d..a1a7db52 100644 --- a/isar/README +++ b/isar/README @@ -7,7 +7,7 @@ Contributions from David von Oheimb, Stefan Berghofer, Status: supported Maintainers: David Aspinall, Makarius Wenzel, Stefan Berghofer -Isabelle versions: Isabelle2009 +Isabelle versions: Isabelle2009-2 (earlier versions not guaranteed) Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ =========================================================================== |