Here are some links to related things.
If you have any suggestions
for links to include here, or find broken links, please
.
- Isamode
is an XEmacs front-end for Isabelle. It has a different
feature collection compared with Proof General:
script management is not supported, but there are extensive
menus and shortcuts provided for common Isabelle
commands.
- CtCoq
is an interface for the Coq theorem prover, developed
at INRIA, Sophia Antipolis, as part of
Projet CROAP.
Like Proof General, CtCoq is based on a general approach for
building user-interfaces for theorem provers, although no other
current theorem provers are supported. Unlike Proof General, CtCoq
is based on a graphical environment with structure editing,
created with the Centaur
system.