diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-08-20 18:45:29 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-08-20 18:45:29 +0000 |
| commit | 868947fbcd8253178336af1e87fcb090273b71c0 (patch) | |
| tree | c94ae04577a80556e5fcaff69691dc7f84a1cb3e | |
| parent | a558a68c4d0b236093ac8b7f0dfe94c39a06fa97 (diff) | |
Updated prover versions
| -rw-r--r-- | doc/ProofGeneral.texi | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index e3483b6d..c269aa0a 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -302,7 +302,7 @@ program. Why not adapt Proof General to your favourite proof assitant? @cindex news Proof General 2.1 is mainly a bug fix release over 2.0. There are some -usability enhancements. See the CHANGES files for more information. +usability enhancements. See the CHANGES file for more information. Two new instantiations of Proof General are being worked on. @emph{Isar}, for the new theory language of Isabelle, and @@ -475,6 +475,7 @@ commands}, and @ref{Customizing Proof General}. Proof General comes ready-customised for these proof assistants: +@c FLAG VERSIONS HERE @itemize @bullet @item @b{LEGO Proof General} for LEGO Version 1.3.1@* @@ -484,14 +485,14 @@ All features of Proof General are supported. For more details @xref{LEGO Proof General}. @item -@b{Coq Proof General} for Coq Version 6.2@* +@b{Coq Proof General} for Coq Version 6.3@* @c written by Healfdene Goguen. @c All features of Proof General are supported except multiple files. For more details @xref{Coq Proof General}. @item -@b{Isabelle Proof General} for Isabelle 98-1@* +@b{Isabelle Proof General} for Isabelle 99@* @c written by David Aspinall. All features of Proof General are supported, except for an external tags program. Isabelle Proof General handles theory files as well as ML @@ -510,6 +511,7 @@ with another proof assistant, @end itemize + @node Prerequisites for this manual @section Prerequisites for this manual |