blob: 7e691384511e0d547a57c9e36fe5b41c4b58cce8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
<p>
Here are some links to related things.
<br>
If you have any suggestions
for links to include here, or find broken links, please
<?php hlink("feedback.phtml","contact us","Feedback form")?>.
</p>
<ul>
<li><a href="http://zermelo.dcs.ed.ac.uk/~isamode">Isamode</a>
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.
</li>
</ul>
<ul>
<li><a href="http://www-sop.inria.fr/croap/ctcoq/ctcoq-eng.html">CtCoq</a>
is an interface for the Coq theorem prover, developed
at INRIA, Sophia Antipolis, as part of
<a href="http://www-sop.inria.fr/croap/">Projet CROAP</a>.
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 <a
href="http://www-sop.inria.fr/croap/centaur/centaur.html">Centaur</a>
system.
</li>
</ul>
|
