lower bound for neper's constant

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

index 33a658479329d10443f9b17d9aa528966ef74b08..845367ad1efebcd8482bcc3b79ffa24d30232e9f 100644 (file)
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -2,6 +2,7 @@
  <!--#include virtual="xhtml-header.shtml" -->
  <html>
    <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,15 @@
         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:
+      <ul>
+       <li><a href=http://www.cs.chalmers.se/Cs/Research/Logic/Types/>
+         Types Project</a>
+       <li><a href=http://www.mctafi.math.unipd.it/>McTafi</a></li>
+       <li><a href=http://dama.cs.unibo.it/>Dama</a></li>
+      </ul>
+      </p>
  
        <!--#include virtual="bottombar.shtml" -->
      </div>