]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/matita/matita.shtml
modifiche
[helm.git] / helm / www / matita / matita.shtml
index b06da9bd0b362bbd98e0c9e3fc10c6bc3547856e..0a331f58b03164190e5eb2705941d5cce5e8d976 100644 (file)
       <p>
       </p>
 <!-- <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>
       
       <p>An interactive prover is a software tool aiding the development of 
       formal proofs by man-machine collaboration. It provides a formal language 
@@ -60,7 +53,7 @@
       come equipped with proofs of (some of) their properties.</p>
 
       <p>Matita is currently adopted in the European Union "Certified Complexity" Project
-      <a href="http://cerco.cs.unibo.it/">CerCo<a> for the formal verification of a 
+      <a href="http://cerco.cs.unibo.it/">CerCo</a> for the formal verification of a 
       complexity-preserving compiler from a large subset of C to a microcontroller 
       assembly of the kind traditionally used in embedded systems.
       </p>