Proof General Kit
Proof General Kit is a new component-based architecture for
the Proof General project, based around a uniform protocol for
communication between interactive proof tools, called
Work which is currently in progress includes:
- An Eclipse plugin for Proof General.
See the wiki
for download and installation instructions.
New! Easy installations are now available at
our update site.
- PG Kit broker, the central middleware component of the PG Kit framework.
Binaries are available here:
(NB: this is not currently required by the Eclipse plugin)
- With assistance from Isabelle developers at Munich:
a PGIP-enabled version of Isabelle/Isar.
This is now integrated into the Isabelle distribution
(the CVS version of Isabelle 2007 is most up-to-date).
Schemas and documentation
The ideas behind the Proof General Kit are described in these papers:
Click here to go back to the front page.
Web pages by
Please report issues
on PG trac.
Last modified 21 December 2017.