X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=5da934cdc8aa6661c76a4af35997b6fd49401713;hb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355;hp=68ebc8ad2fc76b3f5dc9aca4c14e6efa2fc8f6d9;hpb=33f5240193f527ef11619d3ae89cdbf2bfcecb07;p=helm.git

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 68ebc8ad2..5da934cdc 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -25,14 +25,9 @@
       <a href="http://www.unibo.it">University of Bologna</a>.
       </p>
 
+      <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 
@@ -51,18 +46,19 @@
       <p>At the same time, proofs are an integrated part of the formalism, allowing, via the 
       <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">Curry Howard 
       isomorphism</a>, a smooth interplay between
-      specification and reasoning: proofs are objects of the language, and
+      specification, implementation and verification: proofs are objects of the language, and
       can be treated as normal data, naturally leading to a programming style
       akin to <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>, 
       where chunks of software 
       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>
       
+      <!--#include virtual="bottombar.shtml" -->
 
     </div>
   </body>