[opentheory-users] Is OpenTheory usable with Coq?

[Yannick Duchêne]

On Sat, 02 Jan 2016 00:00:29 +0100
"Rob Arthan" <rda at lemma-one.com> wrote:

> The ProofPower user interface (called xpp) is at heart just a simple mouse- and menu -driven wisiwyg text editor that lets you execute selections from the text you are editing in the read-eval-print loop of an interactive program. I routinely use it to develop scripts not just for ProofPower but for HOL Light, HOL4 and other programs like sh, bc and gnuplot. I believe it was quite popular for developing HOL Light code with some of the Flyspeck team in Vietnam.
> 
> Regards,
> 
> Rob.
> 

Oh, thanks for the tip! I though ProofPower was only a prover which was to be used with Emacs. I never suspected it has an editor … will give it a try.