prova

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 4c9e166c5169b31ee651f5c45b2b84cc830e6a67..a68b488302a0d40c85534cfa594e9798211f0722 100644 (file)
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -11,13 +11,6 @@
     <!--#include virtual="news.shtml" -->
     <div class="main">
 
-      <div class="topimage">
-       <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">
       Matita (that means <em>pencil</em> in italian) is an experimental, 
        interactive theorem prover under development at the 
@@ -27,79 +20,7 @@
 
 <!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
 
-      <p class="spaced">
-      <span class="screenshots">
-       <a class="quiet" href="images/screenshot-matita.png">
-         <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
-       </a>
-      </span>
-      
-      Matita is based on the 
-      Calculus of (Co)Inductive Constructions, and is compatible, at some
-      extent, with <a href="http://coq.inria.fr">Coq</a>.
-      It is a reasonably small and simple application, whose 
-      architectural and software complexity is meant to be mastered by 
-      students, providing a tool particularly suited for testing innovative 
-      ideas and solutions.
-      Matita adopts a tactic based editing mode; (XML-encoded) proof objects
-      are produced for storage and exchange. 
-      </p>
-      
-      <p class="spaced"> 
-      <span class="screenshots">
-         <a class="quiet" href="images/screenshot-matita-href.png">
-           <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
-         </a>
-         <a class="quiet" href="images/screenshot-matita-selection.png">
-           <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
-         </a>
-       </span>
-      The graphical interface has been inspired by CtCoq and
-      <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
-      It supports high quality bidimensional rendering of
-      proofs and formulae transformed on-the-fly to 
-      <a href="http://www.w3.org/Math/">MathML</a> markup</p>
-
-      <p class="spaced">
-      <span class="screenshots">
-         <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
-           <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
-         </a>
-         <a class="quiet" href="images/screenshot-cicbrowser-query.png">
-           <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
-         </a>
-         <!--
-         <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
-           <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
-         </a>
-         -->
-      </span>
-      
-      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
-      content-based queries</a>; </p>
-
-      <p class="spaced">
-       <span class="screenshots">
-         <a class="quiet" href="images/screenshot-tinycals.png">
-           <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
-         </a>
-       </span>
-       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>
   </body>
 </html>