Fixed nasty bug in superposition and freshing of clauses

[helm.git] / helm / www / matita / matita.shtml
diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml

index 33a658479329d10443f9b17d9aa528966ef74b08..4c9e166c5169b31ee651f5c45b2b84cc830e6a67 100644 (file)
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -1,7 +1,8 @@
-<!-- $Id$ -->
  <!--#include virtual="xhtml-header.shtml" -->
-<html>
+<!-- $Id$ -->
+<html xmlns="http://www.w3.org/1999/xhtml">
    <head>
+    <meta name="keywords" content="Matita, prover, assistant" />
      <title>Matita - Home Page</title>
      <!--#include virtual="xhtml-meta.shtml" -->
    </head>
@@ -11,7 +12,10 @@
      <div class="main">
  
        <div class="topimage">
-       <img src="images/matita-text-big.png" alt="Big Matita label" />
+       <img src="images/matita-text-big.png" alt="Matita" />
+       <a href="matita_it.shtml">
+         <img src="flags/wit.gif" alt="italian flag" />
+        </a>
        </div>
  
        <p class="spaced">
@@ -71,7 +75,7 @@
           -->
        </span>
        
-      The knowledge base can be 
+      The <a href="library.shtml">knowledge base</a> can be 
        <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
        (locally or on the World Wide Web) and 
        <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
@@ -86,6 +90,14 @@
         The tactical language, part of the proof language, has
         step-by-step semantics, enabling inspection and replaying of deeply
         structured proof scripts. </p>
+        
+      <p>Matita is partially supported by the following Projects: </p>
+      <ul>
+        <li><a href="http://www.cs.chalmers.se/Cs/Research/Logic/Types/">
+          Types Project</a></li>
+       <li><a href="http://www.mctafi.math.unipd.it/">McTafi</a></li>
+       <li><a href="http://dama.cs.unibo.it/">Dama</a></li>
+      </ul>
  
        <!--#include virtual="bottombar.shtml" -->
      </div>