Recently there has been a flurry of work on the next version of Proof General.
It has quite a number of improvements (see
the file), made
by myself and Markus Wenzel.
The next version is aimed to coincide
(or perhaps pre-empt) the release of Isabelle 99.
At the moment we urgently need somebody from the Coq world to
maintain and improve Coq Proof General,
since Patrick Loiseleur
can no longer work on it.
Support from the Coq community is vital for Proof General to
be a useful tool there.
Please offer to help, it needn't be
heavy commitment.
- David.
I've just returned from the
Types Summer School, Giens, France
where Proof General was used for a class of
about 50 students who were learning
Coq, Isabelle, and LEGO. I received
many useful comments and feedback,
which will be
used to improve the next version.
Thanks to everyone who gave suggestions and bug reports
to me, including:
Michael Abbott,
Bernd Grobauer,
Sebastian Skalberg,
Thierry Massart,
Darmalingum Muthiayen.
- David.
Print pictures from the new gallery of publicity shots of Proof General!
Proof General version 2.1 is released.
Check the file
for a summary of changes since Proof General 2.0.
It is recommended that all users upgrade except
those still using Isabelle 98-1.
Proof General 2.1 supports only the 99 version of Isabelle.
New Proof General web pages go live!
The general is now more serious looking. Appropriate, because there are some serious improvements in the pipeline... Before that, we will release Proof General 2.1, mainly a bug-fix improvement of 2.0.
Please explore the new web pages and report any problems or suggestions to . Please also try out the latest pre-release of Proof General, this is the final chance to get fixes and tweaks sorted before 2.1.
A new instantiation of Proof General has been added by Paul Callaghan for Plastic, a new proof assistant based on Luo's Typed Logical Framework and implemented in Haskell.
A new instantiation of Proof General has been added by Markus Wenzel for Isabelle/Isar, a new proof language for Isabelle to be included with Isabelle 99.