ProverEditor v.0.1.0

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.