diff options
Diffstat (limited to 'html/links.phtml')
| -rw-r--r-- | html/links.phtml | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/html/links.phtml b/html/links.phtml index 044fd1b9..87fb489c 100644 --- a/html/links.phtml +++ b/html/links.phtml @@ -7,7 +7,7 @@ for links to include here, or find broken links, please </p> <ul> -<li><a href="http://www.dcs.ed.ac.uk/home/da/Isamode">Isamode</a> +<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 @@ -15,3 +15,17 @@ for links to include here, or find broken links, please 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> |