This editor is used to edit interactive theorem prover files within
Eclipse.
It is made to use with Coq,
and in a near future PVS and other
provers.
It uses a lightweight approach: easy to extend,
with just a minimal set of commands.
For more technical informations about it, see the
gforge repository.
1 Installation and requirements
2 Basic Configurations
These configurations are mandatory if you want Prover Editor to work.
3 Some uses
ProverEditor will be part of the Mobius
tool suite.
This documentation is maintained since the first birthday of
ProverEditor which
was once CoqEditor for Eclipse, september the 25th 2006, and it was
generated on the 27th September, 2006.
This document was translated from LATEX by
HEVEA.