Renamed file

1 files changed, 71 insertions, 0 deletions

diff --git a/html/links.html b/html/links.html
new file mode 100644
index 00000000..32ac9782
--- /dev/null
+++ b/html/links.html
@@ -0,0 +1,71 @@
+<h2>Related projects</h2>
+<p>
+Here are some links to related things.  
+If you have any suggestions 
+for links to include here, 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>
+<ul>
+<li>
+  <a href="http://www.ags.uni-sb.de/~omega/">OMEGA</a> is
+  a collection of web-based distributed tools for supporting
+  theorem proving.
+</li>
+</ul>
+<ul>
+<li>
+  <a href="http://www.dcs.gla.ac.uk/prosper/">Prosper</a> is a project
+  to develop an extensible, open proof tool architecture for
+  incorporating formal verification into industrial CAD/CASE tool
+  flows and design methodologies. The tools include novel
+  user-friendly interfaces.
+</li>
+</ul>
+<ul>
+<li>
+  As a possible foundation for generic proof environments,
+  <a href="http://www.nag.co.uk/projects/openmath/omsoc/">OpenMath</a>
+  is a standard representation form for mathematical objects, which
+  links in with the <a href="http://www.w3.org/Math/">MathML</a>
+  markup language.
+</li>
+</ul>
+<ul>
+<li>
+  <a href="http://www.mrg.dist.unige.it/omrs/index.html">Open Mechanized Reasoning System (OMRS)</a>
+</li>
+</ul>
+<ul>
+<li>
+  <a href="http://www.cs.unibo.it/~asperti/HELM/home.html">Hypertextual Electronic Library of Mathematics (HELM)</a>
+</li>
+</ul>
+<ul>
+<li>
+  <a href="http://eti.cs.uni-dortmund.de:8080/servlet/ETI">ETI</a>
+</li>
+</ul>