Renamed file

1 files changed, 0 insertions, 71 deletions

diff --git a/html/links.phtml b/html/links.phtml
deleted file mode 100644
index 32ac9782..00000000
--- a/html/links.phtml
+++ /dev/null
@@ -1,71 +0,0 @@
-<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>